arnaucube.com/blog/labrador.html
blog/labrador.htmlRaw
1<!DOCTYPE html>
2<html lang="en">
3
4 <head>
5 <meta name="description" content="Overview of how the post-quantum lattice-based SNARK scheme Labrador works." />
6 <meta charset="utf-8">
7 <title> Notes on Labrador, a lattice-based SNARK scheme - arnaucube - blog</title>
8 <meta name="title" content=" Notes on Labrador, a lattice-based SNARK scheme - arnaucube - blog">
9 <meta name="description" content="Overview of how the post-quantum lattice-based SNARK scheme Labrador works.">
10
11 <meta property="og:title" content=" Notes on Labrador, a lattice-based SNARK scheme - arnaucube - blog" />
12 <meta property="og:description" content="Overview of how the post-quantum lattice-based SNARK scheme Labrador works." />
13 <meta property="og:url" content="https://arnaucube.com/blog/labrador.html" />
14 <meta property="og:type" content="article" />
15 <meta property="og:image" content="https://arnaucube.com/blog/" />
16 <meta name="twitter:title" content=" Notes on Labrador, a lattice-based SNARK scheme - arnaucube - blog">
17 <meta name="twitter:description" content="Overview of how the post-quantum lattice-based SNARK scheme Labrador works.">
18 <meta name="twitter:image" content="https://arnaucube.com/blog/">
19 <meta name="twitter:card" content="summary_large_image">
20 <meta name="author" content="arnaucube">
21
22 <link rel="icon" type="image/png" href="img/logoArnauCubeFavicon.png">
23
24 <meta name="viewport" content="width=device-width, initial-scale=1">
25
26 <link href="css/bootstrap.min.css" rel="stylesheet">
27 <link rel="stylesheet" href="css/style.css">
28
29 <!-- highlightjs -->
30 <!-- <link rel="stylesheet" href="js/highlightjs/atom-one-dark.css"> -->
31 <link rel="stylesheet" href="js/highlightjs/atom-one-light.css">
32 <!-- <link rel="stylesheet" href="js/highlightjs/gruvbox-dark.css"> -->
33 <script src="js/highlightjs/highlight.pack.js"></script>
34
35 <!-- katex -->
36 <link rel="stylesheet" href="js/katex/katex.min.css">
37 </head>
38
39 <body>
40
41 <!-- o_gradient_background" -->
42 <nav id="mainNav" class="navbar navbar-default navbar-fixed-top"
43 style="height:50px;font-size:100%;">
44 <div class="container">
45 <div style="float:left;">
46 <a href="/blog" style="color:#000;display:inline-block;">blog</a>
47 <span style="margin-right:20px; margin-left:20px;">|</span>
48 <a href="/blog/notes.html" style="font-size:90%;color:#000;display:inline-block;">notes</a>
49 </div>
50 <div style="float:right;">
51 <a href="/" style="color:#000;display:inline-block;margin-right:10px;">arnaucube.com</a>
52 <div class="onoffswitch" style="margin-left:0px;display:inline-block;" title="change theme">
53 <input onclick="switchTheme()" type="checkbox" name="onoffswitch" class="onoffswitch-checkbox"
54 id="themeSwitcher">
55 <label class="onoffswitch-label" for="themeSwitcher"></label>
56 </div>
57 </div>
58 </div>
59 <!-- <img style="height:5px; width:100%; margin-top:8px;" src="img/gradient-line.jpg" /> -->
60 </nav>
61
62
63
64 <div class="container" style="margin-top:0px;max-width:800px;">
65 <h1>Notes on Labrador, a lattice-based SNARK scheme</h1>
66
67<p><em>2026-06-11</em></p>
68
69<p>I was curious on how (post-quantum) lattice-based SNARKs would work, and since I had a bit of time these past days, I’ve been reading the <a href="https://eprint.iacr.org/2022/1341.pdf">LaBRADOR paper</a>, by Ward Beullens and Gregor Seiler. This post tries to explain the intuition and steps not explicitly shown in the paper, which helped me understanding it.</p>
70
71<p>The structure of this post is the following:</p>
72
73<div id="toc"></div>
74
75<h2>Notation</h2>
76
77<p>The paper uses <span class="math inline">\(\vec{z} \in R^n\)</span> to indicate a vector of length <span class="math inline">\(n\)</span>; for simplicity, in this post I’ll use <span class="math inline">\(z \in R^n\)</span>, since it is already clear that we’re working with a vector since we use <span class="math inline">\(\in R^n\)</span>.</p>
78
79<p>Also, will use <span class="math inline">\(i \in [n]\)</span> to indicate <span class="math inline">\(i = 1, \ldots, n\)</span>. And <span class="math inline">\((a_{ij})\)</span> denotes the matrix with all the <span class="math inline">\(a_{ij}\)</span> values as entries.</p>
80
81<h2>A bit of background on lattices</h2>
82
83<h3>Lattices intro</h3>
84
85<p>Intuitively, think of lattices as a discrete version of finite-dimensional vector spaces. In the same way that vector spaces span over some basis vectors <span class="math inline">\(\{ b_i ~|~ i \in [n] \}\)</span> in a field, lattices span over the basis in a ring:</p>
86<p><span class="math display">\[\mathcal{L} = \mathcal{L}(B) := B \cdot \mathbb{Z}^k = \{ \sum_{i=1}^k z_i \cdot b_i ~|~ z_i \in \mathbb{Z} \}\]</span></p><p>for a basis <span class="math inline">\(B = \{ b_1, \ldots, b_k \}\)</span> (which since they are a basis, they are linearly independent). <span class="math inline">\(k\)</span> is the rank of the basis, and we restrict our attention to <em>full-rank</em> lattices where <span class="math inline">\(k=n\)</span>.</p>
87
88<p>Since we’re at the lattices realm, we work with the polynomial ring <span class="math inline">\(R_q = \mathbb{Z}_q[X]/(X^d + 1)\)</span>, and particularly in Labrador we pick <span class="math inline">\(q\)</span> and <span class="math inline">\(d\)</span> such that <span class="math inline">\(X^d + 1\)</span> splits in two irreducible factors <span class="math inline">\(\pmod q\)</span>.</p>
89
90<p><br></p>
91
92<p>To provide a bit of more intuition, we can relate it to the <em>algebraic coding theory</em> concept of <em>sphere packing problem</em>, where in lattices we use short vectors and in coding theory we’re interested into low weighted codewords. Both in lattices and coding theory we have q-ary {lattices/matrices} respectively and also parity check {lattices/matrices} respectively.</p>
93
94<div style="text-align:center;">
95<img style="width:70%"
96src="img/posts/labrador/lattice-spherepackingproblem.png"></img>
97<br>
98<i></i>
99</div>
100
101<h3>MSIS problem</h3>
102
103<p><em>MSIS</em> problem stands for <em>Module Short Integer Solution</em> problem, and it is as follows:</p>
104
105<p>Given a uniformly random matrix <span class="math inline">\(A \in^R R_q^{n \times m}\)</span>, with columns <span class="math inline">\(a_i \in R_q^n\)</span>, find a non-zero integer vector <span class="math inline">\(z \in R^m\)</span> of norm <span class="math inline">\(||z|| \leq \beta\)</span> such that</p>
106<p><span class="math display">\[A \cdot z = \sum_i a_i \cdot z_i = 0 \in R_q^n\]</span></p>
107<blockquote>
108<p><em>Remarks:</em></p>
109
110<ul>
111<li>without <span class="math inline">\(||z|| \leq \beta\)</span>, it is easy to find a solution via <a href="https://math.libretexts.org/Courses/Palo_Alto_College/College_Algebra/05:_Systems_of_Equations_and_Inequalities/5.04:_Solving_Systems_with_Gaussian_Elimination">Gaussian elimination</a>.</li>
112<li><span class="math inline">\(\beta < q\)</span>, because otherwise <span class="math inline">\(z=(q, 0, \ldots, 0) \in R^m\)</span> would always be a valid solution.</li>
113<li><span class="math inline">\(\beta\)</span> and <span class="math inline">\(m\)</span> must be large enough so that a solution is guaranteed to exist, usually <span class="math inline">\(\beta \geq \sqrt{\hat{m}}\)</span> and <span class="math inline">\(m \geq \hat{m}\)</span> where <span class="math inline">\(\hat{m}\)</span> is the smallest integer greater than <span class="math inline">\(n \log q\)</span>.</li>
114</ul>
115</blockquote>
116
117<p>So overall when doing lattice-based cryptography, we will be interested into keeping the values <em>short</em>, aka. of small norm.</p>
118
119<p>Specifically, Labrador relies on the hardness of finding short solutions to linear equations over polynomial rings.</p>
120
121<p><br></p>
122
123<p>With this in mind, usually a common trick used when doing operations is to decompose the values with small bases, so that we can represent them while keeping the norm low. We will also use this in Labrador.</p>
124
125<h3>Ajtai commitments</h3>
126
127<p>We use a variant of the Ajtai commitments, where the messages are ring elements with small norms.</p>
128
129<p>For a sampled random matrix <span class="math inline">\(A \in^R R_q^{n \times m}\)</span>, and given <span class="math inline">\(x \in R^m\)</span> as input, where <span class="math inline">\(||x|| \leq \beta\)</span>, the Ajtai commitment is defined as <span class="math inline">\(cm := A \cdot x \in R_q^n\)</span>.</p>
130
131<p>In other words, Ajtai commitments are essentially MSIS instances.</p>
132
133<p>Notice that this is binding but it is not hiding, but we could make it hiding by appending a small random veector to <span class="math inline">\(x\)</span>.</p>
134
135<h2>Labrador constraints</h2>
136
137<p>As usual in SNARK schemes, we have the witness, denoted <span class="math inline">\(s= s_1, \ldots, s_r\)</span>, where each <span class="math inline">\(s_i \in R_q^n\)</span>, ie. the witness is a vector of <span class="math inline">\(r\)</span> vectors of ring elements.</p>
138
139<p>And since we’re at the lattices world and we’re using the assumptions of SIS and Module-SIS, the witness values are “short”, that is, their norm is bounded by some parameter: <span class="math inline">\(\sum_{i=1}^r || s_i ||_2^2 \leq \beta^2\)</span>.</p>
140
141<p>While in other SNARK systems we worked with constraints in the shape of R1CS or Plonkish, LaBRADOR defines its constraints as</p>
142<p><span class="math display">\[\boxed{
143f(s) = \sum_{i, j}^r a_{ij} \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \phi_i, s_i \rangle + b = 0
144}
145\]</span></p><p>where <span class="math inline">\(s_i, \phi_i \in R_q^n\)</span>, and <span class="math inline">\(a_{ij}, b \in R_q\)</span>.</p>
146
147<p>There are two different families of constraints, which are evaluated differently:</p>
148
149<ul>
150<li><span class="math inline">\(\mathcal{F}\)</span> family, which are those constraints where the entire polynomial must evaluate to zero, ie. <span class="math inline">\(f(s) = 0\)</span></li>
151<li><span class="math inline">\(\mathcal{F}~'\)</span> family, which are those constraints where we’re only interested in their constant term being zero, ie. <span class="math inline">\(ct( f'(s) ) = 0\)</span></li>
152</ul>
153
154<p>To avoid future doubts, let’s write down what are some constant values:</p>
155
156<ul>
157<li><span class="math inline">\(r\)</span>: amount of witness vectors <span class="math inline">\(s_1, \ldots, s_r\)</span></li>
158<li><span class="math inline">\(K = |\mathcal{F}|\)</span>: amount of original constraints of fully vanishing dot products</li>
159<li><span class="math inline">\(L = |\mathcal{F}~'|\)</span>: amount of original constraints where the constant term is zero</li>
160</ul>
161
162<!--
163(HIDDEN)
164> *Side derailed observation*: since Labrador works with $\mathbb{Z}_q[X]/(X^d + 1)$, where $q, d$ are such that $X^d + 1$ splits in two irreducible factors $\pmod q$, this is a ring, the polynomial ring $R_q$.
165>
166> But imagine for a moment (only imagine, since in many lattice-based cryptography this is not the case) that we pick $q, d$ parameters such that $X^d+1$ is irreducible, then we would have $\mathbb{Z}_q[X]/(X^d+1)$ being a finite field, $\mathbb{F}_{q^d}$; and then, the set of solutions satisfying the family $\mathcal{F}$ would be an *algebraic variety*, which is an interesting algebraic object, although not so useful in the context where we're now. But this is not the case, and in our case the $X^d+1$ that splits into two irreducible factors so that it ensures that through the protocol we can find challenges that are both computationally *short* and invertible when subtracted ([iacr:2017-523](https://eprint.iacr.org/2017/523)).
167-->
168
169<h2>Protocol</h2>
170
171<p>For the rest of this post, I’ll use colours to easily identify the different concepts across the various equations of the protocol.</p>
172
173<p>We start from the <em>original</em> constraints. Those are both, the fully vanishing constraints of the family <span class="math inline">\(\mathcal{F}\)</span> and the constraints where the constant term is zero of the family <span class="math inline">\(\mathcal{F}~'\)</span>:</p>
174<p><span class="math display">\[
175f(s) = \sum_{i, j}^r \textcolor{magenta}{a_{ij}} \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \textcolor{blue}{\phi_i}, s_i \rangle - \textcolor{orange}{b} = 0
176\]</span></p><p><span class="math display">\[
177f'(s) = \sum_{i, j}^r \textcolor{magenta}{a'_{ij}} \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \textcolor{blue}{\phi'_i}, s_i \rangle - \textcolor{orange}{b'} ~~such~that~~ ct(f'(s))=0
178\]</span></p><p>In this blog post we will not cover how do we get from the R1CS constraints into the Labrador constraints shape, it can be found in the section 6 of the paper, but the main idea you need to have is that for different kinds of R1CS constraints (binary and non-binary constraints) we can obtain the <span class="math inline">\(f(s)\)</span> and <span class="math inline">\(f'(s)\)</span> Labrador constraints.</p>
179
180<p>Once we have the original constraints, the idea is to do some reductions adding some more constraints, and then do multiple aggregation steps in order to end up having fewer constraints.</p>
181
182<div style="text-align:center;">
183<img style="width:60%"
184src="img/posts/labrador/constraint-polynomials-evolution.jpg"></img>
185<br>
186<i style="color:#374072">$f(s), f'(s)$ are original polynomials, from the mentioned families $\mathcal{F}$ and $\mathcal{F}~'$ respectively,<br>
187$f_{proj}(s), f''(s)$, $F(s)$ are polynomials that we will describe in the following sections.</i>
188</div>
189
190<p><br>
191Labrador reduces proof size through four transformations unfolded over the next sections:</p>
192
193<ol>
194<li>Commit to the witness</li>
195<li>Reduce norm checking with Johnson-Lindenstrauss projections</li>
196<li>Aggregate many constraints into one</li>
197<li>Amortize openings</li>
198<li>Recurse</li>
199</ol>
200
201<h3>1. Committing to the witness</h3>
202
203<p>We name <em>inner commitments</em> the commitments to the original witness. Those commitments are</p>
204<p><span class="math display">\[cm(s_i) = t_i = A \cdot s_i \in R_q^k ~~ \forall i \in [r]\]</span></p><p>But beware, sending all those <span class="math inline">\(r\)</span> commitments would be too costly, so what the protocol does is it commits to them. The issue then is that <span class="math inline">\(t_i\)</span> (the inner commitments) have coefficients that are <span class="math inline">\(\pmod q\)</span>, whose norm would be too big. The trick that the protocol uses, is the one we mentioned at the <a href="#a-bit%20of%20background%20on%20lattices"><em>‘a bit of background on lattices’</em> section</a>, this is, to decompose them into <span class="math inline">\(t_1 \geq 2\)</span> parts with small base <span class="math inline">\(b_1\)</span> before committing, ie.</p>
205<p><span class="math display">\[t_i = t_i^{(0)} + t_i^{(1)} b_1 + \ldots + t_i^{(t_1-1)} \cdot b_1^{t_1 -1}\]</span></p><p>with <span class="math inline">\(|| t_i^{(k)} ||_{\infty} \leq b_1/2\)</span>.</p>
206
207<p>Now, let <span class="math inline">\(t \in R_q^{r \cdot t_1 \cdot k}\)</span> be the concatenation of all decomposition parts of <span class="math inline">\(t_i^{(k)}\)</span>.</p>
208
209<p>The commitment to the original commitment, is named <em>outer commitment</em>, and it is computed as</p>
210<p><span class="math display">\[u_1 = B \cdot t\]</span></p><p>that is</p>
211<p><span class="math display">\[u_1 = \sum_{i=1}^r \sum_{k=0}^{t_1-1} B_{ik} \cdot t_i^{(k)}\]</span></p><p>with <span class="math inline">\(||t|| \leq \gamma_1\)</span> for a fixed norm parameter <span class="math inline">\(\gamma_1\)</span>.</p>
212
213<p>Now, we want to show that <span class="math inline">\(s=(s_1, \ldots, s_r)\)</span> satisfies the norm bound that we mentioned at the <a href="#setup">setup</a> section. But sending <span class="math inline">\(r\)</span> witness to the verifier would be again too costly, so the protocol reduces it through a projection.</p>
214
215<h3>The σ₋₁ trick</h3>
216
217<p>Before going forward with the protocol, we will overview a trick that Labrador uses in order to compute inner products within the polynomial ring realm.</p>
218
219<p><span class="math inline">\(\sigma_{-1}(\pi_i)\)</span> allows us to convert the coefficient-wise vector inner product into a polynomial multiplication relation.</p>
220
221<p>Within the protocol, we want to compute <span class="math inline">\(p_j = \sum_{i=1}^r \langle \pi_i^{(j)}, s_i \rangle\)</span>, but we want to compute it using ring operations, concretely using polynomial multiplication.</p>
222
223<p>Notice that in Labrador, vectors are encoded as polynomials in <span class="math inline">\(R_q\)</span>, ie</p>
224<p><span class="math display">\[a=(a_1, \ldots, a_{n}) ~\longleftrightarrow~ a(x) = \sum_{k=1}^n a_k X^k \in R_q\]</span></p><p>Let <span class="math inline">\(a(x) = \sum_k a_k X^k,~~ b(x) = \sum_k b_k X^k\)</span>, then when computing <span class="math inline">\(a(x) \cdot b(x)\)</span></p>
225<p><span class="math display">\[a(x) b(x) = (\sum_k a_k X^k) \cdot (\sum_k b_k X^k) = \sum_{i,j} a_i b_j X^{i+j}\]</span></p><p>which is different from the dot product that we’re interested in.</p>
226
227<p>We want to only multiply together the coefficients of the equal-index terms, ie. <span class="math inline">\(a_0 b_0 + a_1 b_1 + \ldots + a_{n-1} b_{n-1}\)</span>. Thus we need some trick to force getting only the values when <span class="math inline">\(i=j\)</span>.</p>
228
229<p>The trick is with <span class="math inline">\(\sigma_{-1}\)</span> and getting the constant term of the result of multiplying <span class="math inline">\(\sigma_{-1}(a) \cdot b\)</span>.</p>
230
231<p>Define the automorphism <span class="math inline">\(\sigma_{-1}\)</span> as <span class="math inline">\(\sigma_{-1}(X) = X^{-1}\)</span>, so that <span class="math inline">\(\sigma_{-1}(a(X)) = a(X^{-1}) = \sum_i a_i X^{-i}\)</span>.</p>
232
233<p>Then, when multiplying</p>
234<p><span class="math display">\[\sigma_{-1}(a(X)) \cdot b(X) = \sum_{i,j} a_i b_j X^{j-i}\]</span></p><p>So, when <span class="math inline">\(j=i\)</span>, <span class="math inline">\(X\)</span> will be <span class="math inline">\(0\)</span>; hence the result we’re interested in, the dot product result, will be contained in the constant terms of the result of that multiplication, where the <span class="math inline">\(X^{j-i}=X^0\)</span>.</p>
235
236<p>In other words, <span class="math inline">\(\langle a, b \rangle = ct(\sigma_{-1}(a(X)) \cdot b(X))\)</span>, where <span class="math inline">\(ct\)</span> denotes getting the constant term. That is, applied to the projection case, <span class="math inline">\(\langle \pi_i^{(j)}, s_i \rangle= ct(\sigma_{-1}(\pi_i^{(j)}) \cdot s_i)\)</span>.</p>
237
238<h3>2. Johnson-Lindenstrauss projection</h3>
239
240<p>The main idea here, is that we will use random linear projections that almost preserve the <span class="math inline">\(l_2\)</span>-norm while allowing us to reduce the amount of equations to check, while keeping the bounds in place.</p>
241
242<p>This relies on the Johnson-Lindenstrauss Lemma, which basically is used as instead of revealing all the witnes values <span class="math inline">\(s_1, \ldots, s_r\)</span>, the verifier samples a random linear map <span class="math inline">\(\Pi: \mathbb{Z}_q^{nd} \longrightarrow \mathbb{Z}_q^{256}\)</span>, and then the prover reveals only <span class="math inline">\(\Pi \cdot s\)</span>, which has many less elements than the original <span class="math inline">\(s\)</span> vector.</p>
243
244<p>And the Johnson-Lindenstrauss Lemma guarantees that <span class="math inline">\(||\Pi s||\)</span> contains almost the same norm information as <span class="math inline">\(||s||\)</span> with very high probability.</p>
245
246<p>In practice, verifier samples <span class="math inline">\(\Pi_i = (\pi_i^{(j)})_j \in \chi^{256 \times nd}\)</span>, the prover computes <span class="math inline">\(p_j = \sum_{i=1}^r \langle \pi_i^{(j)}, s_i \rangle\)</span>, and the verifier checks that <span class="math inline">\(||p|| \leq \sqrt{128} \beta\)</span>.</p>
247
248<p>So at this point, in the family <span class="math inline">\(\mathcal{F}~'\)</span>, we have the original constraints, without any projection related stuff:</p>
249<p><span class="math display">\[
250f'(s) = \sum_{i, j}^r \textcolor{magenta}{a'_{ij}} \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \textcolor{blue}{\phi'_i}, s_i \rangle + \textcolor{orange}{b'} = 0
251\]</span></p><p>And the projection constraints, which encode the check for the J-L projection in the Labrador constraints shape:</p>
252
253<p>Notice that the projection equation, <span class="math inline">\(p_j = \sum_{i=1}^r \langle \sigma_{-1}(\pi_i^{(j)}), s_i \rangle\)</span> is also</p>
254<p><span class="math display">\[\sum_{i=1}^r \langle \sigma_{-1}(\pi_i^{(j)}), s_i \rangle - p_j = 0\]</span></p><p>which looks almost like the Labrador canonical constraints, we just need to add the <span class="math inline">\(a_{ij}\)</span> part. We do it by setting <span class="math inline">\(a_{ij}=0\)</span>:</p>
255<p><span class="math display">\[
256f_{proj}(s) = \sum_{i, j}^r \textcolor{magenta}{0} \cdot \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \textcolor{blue}{\sigma_{-1}(\pi_i^{(j)})}, s_i \rangle - \textcolor{orange}{p_j} = 0
257\]</span></p><p>this is, we set <span class="math inline">\(\textcolor{magenta}{a_{proj,ij}=0}\)</span>, <span class="math inline">\(\textcolor{blue}{\phi_{proj,~i}=\sigma_{-1}(\pi_i^{(j)})}\)</span> and <span class="math inline">\(\textcolor{orange}{b_{proj} = -p_j}\)</span>. In this way we have the projection constraints encoded as Labrador constraints.</p>
258
259<p>Recall that both the original <span class="math inline">\(f'(s)\)</span> constraints, and the projection constraints <span class="math inline">\(f_{proj}(s)\)</span> are in the family <span class="math inline">\(\mathcal{F}~'\)</span>, so that we care about their constant term being zero, not the full polynomial vanishing.</p>
260
261<h3>3. Aggregation steps</h3>
262
263<p>At this point of the protocol, in the family <span class="math inline">\(\mathcal{F}~'\)</span>, we have <span class="math inline">\(L\)</span> original constraints <span class="math inline">\(f'(s)\)</span> and <span class="math inline">\(256\)</span> projection constraints <span class="math inline">\(f_{proj}(s)\)</span>. The idea now is to linearly combine them into fewer constraints.</p>
264
265<p>The verifier sends the challenges <span class="math inline">\(\psi^{(k)} \in^R (\mathbb{Z}_q)^L\)</span> and <span class="math inline">\(w^{(k)} \in^R (\mathbb{Z}_q)^{256}\)</span>, which the prover will use to compute the random linear combinations of the constraints we have so far, which preserves the validity while reducing the number of constraints.</p>
266
267<h4>3.1. 1st aggregation</h4>
268
269<p>The prover linearly combines</p>
270
271<ul>
272<li>the <span class="math inline">\(L\)</span> original constraints from <span class="math inline">\(f'(s)\)</span></li>
273<li>the <span class="math inline">\(256\)</span> constraints that prove the Johnson-Lindenstrauss projection, <span class="math inline">\(f_{proj}(s)\)</span></li>
274</ul>
275
276<p>as follows</p>
277<p><span class="math display">\[
278f''^{(k)}(s) =
279\sum_{l=1}^L \psi_l^{(k)} \cdot f'^{(l)}(s)
280+
281\sum_{j=1}^{256} w_j^{(k)} \cdot f_{proj}(s)
282=
283\\
284= \underbrace{ \sum_{l=1}^L \psi_l^{(k)} \cdot f'^{(l)}(s) }_{(i.)~ \text{lin.comb. of the original constraints}}
285+
286\underbrace{ \sum_{j=1}^{256} w_j^{(k)} \cdot ( \langle \sigma_{-1}(\pi_i^{(j)}), s_i \rangle -p_j) }_{(ii.)~ \text{lin.comb. of the 256 projection constraints}}
287\]</span></p><p>First we will tackle <span class="math inline">\((i.)\)</span>. Recall that <span class="math inline">\(f'(s) = \sum_{i, j}^r a_{ij}' \cdot \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \phi_i', s_i \rangle + b'\)</span>, so by distributing the challenge <span class="math inline">\(\psi_l^{(k)}\)</span>,</p>
288<p><span class="math display">\[
289(i.):~
290\sum_l \psi_l^{(k)} \cdot f'^{(l)}(s) =
291\sum_l \psi_l^{(k)} \cdot \left(
292 \sum_{i,j} a_{ij}^{'(l)} \cdot \langle s_i, s_j \rangle
293 + \sum_i \langle \phi_i^{'(l)}, s_i \rangle - b_0^{'(k)}
294\right)\\
295=
296\underbrace{
297\sum_{i,j} \left( \sum_l \psi_l^{(k)} \cdot a_{ij}^{'(l)} \right) \cdot \langle s_i, s_j \rangle
298}_{(i.A)}
299\underbrace{
300+ \sum_i \left( \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)} \right) \cdot s_i
301- \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
302}_{(i.B)}
303\]</span></p><p>For the <span class="math inline">\((i.A)\)</span> part, we can set</p>
304<p><span class="math display">\[\textcolor{magenta}{a_{ij}^{''(k)}} = \sum_{l=1}^L \psi_l^{(k)} \cdot a_{ij}^{'(l)}\]</span></p><p>so that:</p>
305<p><span class="math display">\[
306(i.A):~
307 \sum_{i,j} \left( \sum_l \psi_l^{(k)} \cdot a_{ij}^{'(l)} \right) \cdot \langle s_i, s_j \rangle ~=~ \sum_{i,j} \textcolor{magenta}{a''^{(k)}_{ij}} \cdot \langle s_i, s_j \rangle
308\]</span></p><p>Now tackle <span class="math inline">\((ii.)\)</span>:</p>
309<p><span class="math display">\[
310(ii.):~ \sum_{j=1}^{256} w_j^{(k)} \cdot \big( \langle \sigma_{-1}(\pi_i^{(j)}), s_i \rangle - p_j \big) = \sum_i \langle \sum_j w_j^{(k)} \sigma_{-1}(\pi_i^{(j)}),~ s_i \rangle
311- \sum_j w_j^{(k)} \cdot p_j
312\]</span></p><p>Now let’s put together <span class="math inline">\((i.B)\)</span> and <span class="math inline">\((ii)\)</span>:</p>
313<p><span class="math display">\[
314\overbrace{
315 \textcolor{green}{
316 \sum_i ( \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)} ) \cdot s_i
317 }
318 \textcolor{blue}{
319 - \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
320 }
321}^{(i.B)}
322+
323\overbrace{
324 \textcolor{orange}{
325 \sum_i \langle \sum_j w_j^{(k)} \sigma_{-1}(\pi_i^{(j)}),~ s_i \rangle
326 }
327 \textcolor{red}{
328 - \sum_j w_j^{(k)} \cdot p_j
329 }
330}^{(ii.)}
331=\\~\\
332=
333 \sum_i
334\textcolor{green}{
335 \big\langle
336 \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)}
337 }
338 +
339 \textcolor{orange}{
340 \sum_l w_j^{(k)} \cdot \sigma_{-1}(\pi_i^{(j)}), s_i
341 \big\rangle
342 }
343 +
344 \textcolor{blue}{
345 \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
346 }
347 +
348 \textcolor{red}{
349 \sum_j w_j^{(k)} \cdot p_j
350 }
351\]</span></p><p>without colors:</p>
352<p><span class="math display">\[
353=
354\sum_i
355 \big\langle
356 \underbrace{
357 \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)}
358 +
359 \sum_l w_j^{(k)} \cdot \sigma_{-1}(\pi_i^{(j)})
360 }_{\phi_i^{''(k)}},
361 s_i
362 \big\rangle
363 +
364 \underbrace{
365 \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
366 +
367 \sum_j w_j^{(k)} \cdot p_j
368 }_{b_0^{''(k)} ~\text{(constant term)}}
369 \\
370 =
371 \sum_{i=1}^r \langle \textcolor{blue}{\phi_i^{''(k)}}, s_i \rangle - \textcolor{orange}{b_0^{''(k)}}
372\]</span></p><p>So by putting it together with the <span class="math inline">\((i.A)\)</span> part, we get the full <span class="math inline">\(f''^{(k)}(s)\)</span> aggregated constraint:</p>
373<p><span class="math display">\[
374\boxed{
375f''^{(k)}(s) =
376\overbrace{
377\sum_{i,j=1}^r \textcolor{magenta}{a_{ij}^{''(k)}} \cdot \langle s_i, s_j \rangle
378}^{(i.A)}
379+
380\overbrace{
381\sum_{i=1}^r \langle \textcolor{blue}{\phi_i^{''(k)}}, s_i \rangle - \textcolor{orange}{b_0^{''(k)}}
382}^{(i.B) + (ii.)}
383}
384\]</span></p><p>such that <span class="math inline">\(ct(f''^{(k)}(s)) = 0\)</span>.</p>
385
386<p><br></p>
387
388<p>Right now, <span class="math inline">\(f''^{(k)}(s)\)</span> is a constraint where only the constant term evaluates to zero (ie. it is a constraint from the <span class="math inline">\(\mathcal{F}'\)</span> family). However, for the next aggregation step, we need it to be a <em>completely vanishing</em> polynomial, that is, a function from the <span class="math inline">\(\mathcal{F}\)</span> family.</p>
389
390<p>To do so, the prover takes the integer constant <span class="math inline">\(\textcolor{orange}{b_0^{''(k)}}\)</span> and extends it into a full polynomial <span class="math inline">\(\textcolor{orange}{b''^{(k)}}\)</span> so that the newly formed function <span class="math inline">\(f''^{(k)}(s)\)</span> evaluates exactly to zero. The prover then sends these full <span class="math inline">\(b''^{(k)}\)</span> polynomials to the verifier.</p>
391
392<p>To ensure that the prover isn’t cheating by just making up a polynomial that matches the equation, the verifier will check that the constant coefficient of the prover’s <span class="math inline">\(b''^{(k)}\)</span> corresponds to the <span class="math inline">\(b_0^{''(k)}\)</span> value that the verifier computes from the public values and challenges, that is <span class="math inline">\(b_0^{''(k)} \stackrel{?}{=} \langle w^{(k)}, p \rangle + \sum_{l=1}^L \psi_l^{(k)} b_0^{'(l)}\)</span>.</p>
393
394<p><br></p>
395
396<p>Recall that along these past steps, we’ve defined the new <span class="math inline">\(a_{ij}^{''(k)},~ \phi_i^{''(k)},~ b''\)</span> as</p>
397<p><span class="math display">\[\textcolor{magenta}{a_{ij}^{''(k)}} = \sum_{l=1}^L \psi_l^{(k)} \cdot \textcolor{magenta}{a_{ij}^{'(l)}}\]</span></p><p><span class="math display">\[\textcolor{blue}{\phi_i^{''(k)}} = \sum_{l=1}^L \psi_l^{(k)} \textcolor{blue}{\phi_i^{'(l)}} + \sum_{j=1}^{256} w_j^{(k)} \cdot \sigma_{-1}(\textcolor{blue}{\pi_i^{(j)}})\]</span></p><p><span class="math display">\[\textcolor{orange}{b''} = \sum_{i,j=1}^r \textcolor{magenta}{a_{ij}^{''(k)}} \cdot \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \textcolor{blue}{\phi_i^{''(k)}}, s_i \rangle\]</span></p>
398<h4>3.2. 2nd aggregation</h4>
399
400<p>Till here, the 1st aggregation step has taken a random linear combination of the original constant-vanishing constraints and the projection constraints, and linearly combined them into Labrador-shaped constraints.</p>
401
402<p>Now the idea is to random linearly combine the original fully vanishing constraints <span class="math inline">\(f(s)\)</span>, and separately the aggregated <span class="math inline">\(f''(s)\)</span> constraints that come from the original constant-vanishing constraints (<span class="math inline">\(f'(s)\)</span>) and projection constraints (<span class="math inline">\(f_{proj}(s)\)</span>).</p>
403
404<p>The verifier sends the challenges <span class="math inline">\(\alpha \in^R R_q^K,~ \beta \in^R R_q^{\lceil 128/\log{q} \rceil}\)</span>.</p>
405
406<p>Then the prover will compute</p>
407<p><span class="math display">\[
408F(s) = \sum_{k=1}^K \alpha_k \cdot f^{(k)}(s) + \sum_{k=1}^{\lceil 128/ \log q \rceil} \beta_k \cdot f''^{(k)}\\
409=
410\sum_{k=1}^K \alpha_k \cdot \left( \sum_{i, j}^r a_{ij} \langle s_i, s_j \rangle + \sum_{i=1}^r \langle \phi_i, s_i \rangle + b \right)
411+
412\sum_{k=1}^{\lceil 128/ \log q \rceil} \beta_k \cdot
413\left(
414 \sum_{i,j}^r a_{ij}^{''(k)} \langle s_i, s_j \rangle + \sum_i^r \langle \phi_i^{''(k)}, s_i \rangle - b_0^{''(k)}
415\right)
416\]</span></p><p>distribute <span class="math inline">\(\alpha_k\)</span> and <span class="math inline">\(\beta_k\)</span> while keeping the witness values separated</p>
417<p><span class="math display">\[
418= \sum_{i,j=1}^r
419\underbrace{
420 \left( \sum_{k=1}^K \alpha_k a_{ij}^{(k)}
421 +
422 \sum_{k=1}^{\lceil 128/\log q \rceil} \beta_k a_{ij}''^{(k)}
423 \right)
424}_{a_{ij}}
425\langle s_i, s_j \rangle + \sum_{i=1}^r \langle \underbrace{ \left( \sum_{k=1}^K \alpha_k \phi_i^{(k)} + \sum_{k=1}^{\lceil 128/\log q \rceil} \beta_k \phi_i''^{(k)} \right) }_{\phi_i}, s_i \rangle
426\\
427- \underbrace{ \left( \sum_{k=1}^K \alpha_k b^{(k)} + \sum_{k=1}^{\lceil 128/\log q \rceil} \beta_k b''^{(k)} \right) }_{b}
428\]</span></p><p><span class="math display">\[
429\boxed{
430 F(s) = \sum_{i,j} a_{ij} \langle s_i, s_j \rangle + \sum_i \langle \phi_i, s_i \rangle - b
431}
432\]</span></p><p>again, a Labrador-shaped constraint, which in this case encodes the linear combinations of the original <span class="math inline">\(f^{(k)}(s)\)</span> constraints and the <span class="math inline">\(f''^{(k)}(s)\)</span> aggregated constraints, which for a valid witness it satisfies <span class="math inline">\(F(s)=0\)</span>.</p>
433
434<h3>4. Amortization</h3>
435
436<p>Now, at this point we have <span class="math inline">\(r\)</span> witness vectors, which in practice it is too much to deal with. Thus, instead of opening the individual inner commitments <span class="math inline">\(t_i\)</span> by sending all the <span class="math inline">\(s_i\)</span> and then checking the constraint <span class="math inline">\(F(s)\)</span>, the prover opens a random linear combination</p>
437<p><span class="math display">\[z = \sum_{i=1}^r c_i \cdot s_i\]</span></p><p>and its respective committed version</p>
438<p><span class="math display">\[\overline{z} = \sum_{i=1}^r c_i \cdot t_i\]</span></p><p>with challenge polynomials <span class="math inline">\(c_i \in R_q\)</span>.</p>
439
440<p>Then the verifier checks</p>
441<p><span class="math display">\[A \cdot z = \sum_{i=1}^r c_i \cdot t_i\]</span></p><p>which should match since <span class="math inline">\(t_i\)</span> are the commitments to <span class="math inline">\(s_i\)</span> such that <span class="math inline">\(t_i = A s_i\)</span>, so that</p>
442<p><span class="math display">\[A \cdot z = A \cdot \sum_i^r c_i s_i = \sum_i c_i \cdot (A s_i) = \sum_i c_i t_i\]</span></p><p>And also checks that <span class="math inline">\(||z|| \leq \gamma\)</span> which comes from the instantiation parameters, to ensure small norm.</p>
443
444<p><br></p>
445
446<p>The following step is verifying that <span class="math inline">\(F(s)=0\)</span>, but recall that <span class="math inline">\(F(s) = \sum_{i,j} a_{ij} \langle s_i, s_j \rangle + \sum_i \langle \phi_i, s_i \rangle - b\)</span>, and the verifier does not know the values of <span class="math inline">\(s_i\)</span> hence can not compute it.</p>
447
448<p>To do the check, both prover and verifier use what the paper calls <em>garbage polynomials</em>, but intuitively we can think about them as some auxiliary polynomials to do this final check.</p>
449
450<p>Let the <em>garbage polynomials</em> be</p>
451<p><span class="math display">\[g_{ij}= \langle s_i, s_j \rangle,~~~~ h_{ij} = \frac{1}{2} ( \langle \phi_i, s_j \rangle + \langle \phi_j, s_i \rangle )\]</span></p><p>for <span class="math inline">\(i,j \in [r]\)</span>.</p>
452
453<p>The prover will commit to those polynomials early on, before the challenges <span class="math inline">\(c_i\)</span> are generated, so that the prover is not able to select the garbage polynomials based on knowledge of the challenges, which would allow the prover to cheat.</p>
454
455<blockquote>
456<p>Observation: the paper does the commitment to the “garbage” polynomials <span class="math inline">\(g\)</span> and <span class="math inline">\(h\)</span> differently at the protocol conceptual explanation of page 14 and at the protocol description of Figure 2 at page 17.</p>
457
458<p>The conceptual explanation describes the second outer commitment <span class="math inline">\(u_2\)</span> as</p>
459<p><span class="math display">\[u_2 = C g + D h\]</span></p><p>but later at the protocol description, the commitment to <span class="math inline">\(g\)</span> is moved to the outer commitment <span class="math inline">\(u_1\)</span>, leaving only the commitment to <span class="math inline">\(h\)</span> at <span class="math inline">\(u_2\)</span>. So the outer commitments end up being</p>
460<p><span class="math display">\[u_1 = B \cdot t + C \cdot g = \sum_{i=1}^r \sum_{k=0}^{t_1-1} B_{ik} t_i^{(k)} + \sum_{i \leq j} \sum_{k=0}^{t_2-1} C_{ijk} g_{ij}^{(k)}\]</span></p><p><span class="math display">\[u_2 = D \cdot h = \sum_{i \leq j} \sum_{k=0}^{t_1-1} D_{ijk} h_{ij}^{(k)}\]</span></p><p>This is done because the <span class="math inline">\(g_{ij}\)</span> polynomials are independent of all challenges, thus they can be computed at the very beginning of the protocol and included in <span class="math inline">\(u_1\)</span>, allowing a slightly better security proof.</p>
461</blockquote>
462
463<p>Then, the verifier will do the following checks:</p>
464<p><span class="math display">\[(i.)~~~ <z, z> = \sum_{i,j=1}^r g_{ij} c_i c_j\]</span></p><p><span class="math display">\[(ii.)~~~ \sum_{i=1}^r \langle \phi_i, z \rangle \cdot c_i = \sum_{i,j=1}^r h_{ij} c_i c_j\]</span></p><p><span class="math display">\[(iii.)~~~ \sum_{i,j=1}^r a_{ij} g_{ij} + \sum_{i=1}^r h_{ii} -b = 0\]</span></p><p>Where <span class="math inline">\((i.)\)</span> and <span class="math inline">\((ii.)\)</span> are to check the correctness of <span class="math inline">\(g_{ij}\)</span> and <span class="math inline">\(h_{ij}\)</span> respectively, and <span class="math inline">\((iii.)\)</span> is checking the <span class="math inline">\(F(s)=0\)</span> equality through the garbage polynomials <span class="math inline">\(g_{ij}, h_{ij}\)</span>.</p>
465
466<h3>5. Recursion</h3>
467
468<p>At this point, the prover has sent the <em>proof</em> which consists of <span class="math inline">\((z, t, h, g)\)</span>, and the norm checks get grouped into a single norm check <span class="math inline">\(||z||^2 + ||t||^2 + ||g||^2 + ||h||^2 \leq \gamma^2 + \gamma_1^2 + \gamma_2^2\)</span>.</p>
469
470<p>The idea now, is to recurse, encoding the protocol checks into new Labrador constraints, and then performing again the protocol.</p>
471
472<p>First, we simplify the target relation, let <span class="math inline">\(v = t || g || h \in R_q^m\)</span>, so that the norm check becomes</p>
473<p><span class="math display">\[||z||^2 + ||v||^2 \leq \gamma^2 + \gamma_1^2 + \gamma_2^2\]</span></p><p>Now we decompose the witness <span class="math inline">\(z = z^{(0)} + b \cdot z^{(1)}\)</span>, with <span class="math inline">\(z^{(0)}, z^{(1)} \in R_q^n\)</span>, to keep the coefficients with small norm.</p>
474
475<p>Then, the quadratic dot product becomes</p>
476<p><span class="math display">\[\langle z, z \rangle = \langle z^{(0)}, z^{(0)} \rangle + 2b \langle z^{(0)}, z^{(1)} \rangle + b^2 \langle z^{(1)}, z^{(1)} \rangle\]</span></p><p>and we can do the norm check as <span class="math inline">\(||z^{(0)}||^2 + ||z^{(1)}||^2 + ||v||^2 \leq \frac{2}{b^2} \gamma^2 + \gamma_1^2 + \gamma_2^2 = (\beta')^2\)</span>, which implies <span class="math inline">\(||z|| = ||z^{(0)} + b z^{(1)} || \leq (1+b)\beta'\)</span>.</p>
477
478<p>Write the vectors <span class="math inline">\(z^{(0)}, z^{(1)}, v\)</span> as concatenations of vectors:</p>
479<p><span class="math display">\[
480z^{(0)} = s_1 || s_2 || \ldots || s_{\nu}\\
481z^{(1)} = s_{\nu+1} || \ldots || s_{2\nu}\\
482v = s_{2\nu+1} || \ldots || s_{2\nu+ \mu}
483\]</span></p><p>that is <span class="math inline">\(r' = 2 \nu + \mu\)</span> vectors in total.</p>
484
485<p>Observe that the final verifications from the previous section, the checks <span class="math inline">\((i.),~ (ii.),~ (iii.)\)</span> can be done as dot product constraints (ie. Labrador constraints):</p>
486
487<h4>encoding check (i.)</h4>
488
489<p>from the check <span class="math inline">\((i.)\)</span>, <span class="math inline">\(\langle z, z \rangle = \sum_{i,j=1}^r g_{ij} \cdot c_i \cdot c_j\)</span>, since we’ve decomposed <span class="math inline">\(z = z^{(0)} + b z^{(1)}\)</span> then we have</p>
490<p><span class="math display">\[
491\langle z, z \rangle = \langle z^{(0)} + b z^{(1)}, z^{(0)} + b z^{(1)} \rangle\\
492= \langle z^{(0)}, z^{(0)} \rangle + 2b \langle z^{(0)}, z^{(1)} \rangle + b^2 \langle z^{(1)}, z^{(1)} \rangle
493\]</span></p><p>that is, three separate dot products. Then we place</p>
494<p><span class="math display">\[
495z^{(0)} ~\text{into}~ s_1', \ldots, s'_{\nu}\\
496z^{(1)} ~\text{into}~ s_{\nu+1}', \ldots, s'_{2\nu}
497\]</span></p><p>so that</p>
498<p><span class="math display">\[\langle z^{(0)}, z^{(0)} \rangle = \langle s_1', s_1' \rangle + \langle s_2', s_2' \rangle + \ldots + \langle s_{\nu}', s_{\nu}' \rangle\]</span></p><p>and similarly with <span class="math inline">\(\langle z^{(1)}, z^{(1)} \rangle\)</span></p>
499<p><span class="math display">\[\langle z^{(1)}, z^{(1)} \rangle = \langle s_{\nu+1}', s_{\nu+1}' \rangle + \ldots + \langle s_{2\nu}', s_{2\nu}' \rangle\]</span></p><p>and</p>
500<p><span class="math display">\[\langle z^{(0)}, z^{(1)} \rangle = \langle s_1', s_{\nu+1}' \rangle + \langle s_2', s_{\nu+2}' \rangle + \ldots + \langle s_{\nu}', s_{2\nu}' \rangle\]</span></p><p>So that now, it is a matter of setting appropriate <span class="math inline">\(a_{ij}\)</span> values to reshape the original check into a Labrador-shaped constraint:</p>
501
502<ul>
503<li>from <span class="math inline">\(1\)</span> to <span class="math inline">\(\nu\)</span>: if <span class="math inline">\(i=j\)</span>, set <span class="math inline">\(a_{ij}=1,~ 0\)</span> otherwise,</li>
504<li>from <span class="math inline">\(\nu+1\)</span> to <span class="math inline">\(2\nu\)</span>: if <span class="math inline">\(i=j\)</span>, set <span class="math inline">\(a_{ij}=b^2,~ 0\)</span> otherwise,</li>
505<li>from <span class="math inline">\(2\nu\)</span> to <span class="math inline">\(2\nu+\mu\)</span>: if <span class="math inline">\(j=i+\nu\)</span>, set <span class="math inline">\(a_{ij}=b\)</span>. And since the <span class="math inline">\((a_{ij})\)</span> matrix is symmetric, then <span class="math inline">\(a_{ji}=b\)</span>, which implies that when both combined we get <span class="math inline">\(2b\)</span>.</li>
506</ul>
507
508<p>Therefore, we can perform the <span class="math inline">\(\langle z, z \rangle\)</span> with the decompositions <span class="math inline">\(z^{(0)},~ z^{(1)}\)</span>.</p>
509
510<h4>encoding check (ii.)</h4>
511
512<p>The next check is <span class="math inline">\((ii.)\)</span>, <span class="math inline">\(\sum_{i=1}^r \langle \phi_i, z \rangle \cdot c_i = \sum_{i, j = 1}^r h_{ij} c_i c_j\)</span>. Reshape it into</p>
513<p><span class="math display">\[\sum_{i=1}^r \langle \phi_i \cdot c_i, z \rangle - \sum_{i, j = 1}^r (c_i c_j)\cdot h_{ij} = 0\]</span></p><p>and, recall that we set</p>
514<p><span class="math display">\[
515z^{(0)} = s_1 || s_2 || \ldots || s_{\nu}\\
516z^{(1)} = s_{\nu+1} || \ldots || s_{2\nu}\\
517v = s_{2\nu+1} || \ldots || s_{2\nu+ \mu}
518\]</span></p><p>also recall that <span class="math inline">\(v=t || g || h\)</span>. Thus, similarly as for the check <span class="math inline">\((i.)\)</span>,</p>
519
520<ul>
521<li>from <span class="math inline">\(1\)</span> to <span class="math inline">\(\nu\)</span>: <span class="math inline">\(\phi_i^{(k)} = \sum \phi_i c_i\)</span>,</li>
522<li>from <span class="math inline">\(\nu+1\)</span> to <span class="math inline">\(2\nu\)</span>: <span class="math inline">\(\phi_i^{(k)} = \sum \phi_i c_i \cdot b\)</span>,</li>
523<li>from <span class="math inline">\(2\nu\)</span> to <span class="math inline">\(2\nu+\mu\)</span>: <span class="math inline">\(\phi_i^{(k)} = - (c_i c_j)\)</span>.</li>
524</ul>
525
526<h4>encoding check (iii.)</h4>
527
528<p>For the check <span class="math inline">\((iii.)\)</span>, <span class="math inline">\(\sum a_{ij} g_{ij} + \sum h_{ii} - b =0\)</span>, recall again that <span class="math inline">\(g_{ij}, h_{ij}\)</span> are inside <span class="math inline">\(v\)</span>, so it is just a matter of setting <span class="math inline">\(a_{ij}=a_{ij}\)</span> and <span class="math inline">\(a_{ij}=1\)</span> at their corresponding positions, and <span class="math inline">\(b^{(k)}=b\)</span>.</p>
529
530<p>With this, we can encode the checks <span class="math inline">\((i.),~ (ii.),~ (iii.)\)</span> into the Labraddor constraint shape</p>
531<p><span class="math display">\[g^{(k)}(s') = \sum_{i,j=1}^{r'} a_{ij}^{(k)} \langle s_i', s_j' \rangle + \sum_i^{r'} \langle \phi_i^{(k)}, s_i' \rangle - b^{(k)} = 0\]</span></p><p>with <span class="math inline">\(s' := z^{(0)} || z^{(1)} || v\)</span>, where <span class="math inline">\(v=t ||g||h\)</span>.</p>
532
533<h4>encoding commitments checks</h4>
534
535<p>Similarly we encode he commitments checks. We had <span class="math inline">\(Az = \sum c_i t_i\)</span>, which we can do in a dot product constraint as</p>
536<p><span class="math display">\[\langle A_{row}, z \rangle - \sum c_i \cdot ~ (t_i)_{row} = 0\]</span></p><p>which in a similar fashion as the checks <span class="math inline">\((i.), (ii.), (iii.)\)</span>, we can reshape it into a Labrador constraint, since the inner commitments <span class="math inline">\(t_i\)</span> are placed inside <span class="math inline">\(v\)</span>.</p>
537
538<p><br></p>
539
540<p>And for the outer commitments <span class="math inline">\(u_1,~ u_2\)</span>, as we saw in the section [<a href="#4.-amortization">4. Amortization</a>] we want</p>
541<p><span class="math display">\[
542u_1 = B \cdot t + C \cdot g\\
543u_2 = D \cdot h
544\]</span></p><p>which we can encode as</p>
545<p><span class="math display">\[
546\langle B_{row}, t \rangle + \langle C_{row}, g \rangle = (u_1)_{row}\\
547\langle D_{row}, h \rangle = (u_2)_{row}
548\]</span></p><p>which, as before, we can also reshape into the dot product Labrador constraints.</p>
549
550<p><br></p>
551
552<p>The paper mentions that <a href="https://giphy.com/gifs/67-six-seven-john-chungus-08uBcURaMq6vA93TGc">6 or 7</a> iterations of the recursive protocol give the best results, where at each recursion the witness shrinks down from <span class="math inline">\(|s^{(i)}|\)</span> into <span class="math inline">\(|s^{(i)}|^{2/3}\)</span>.</p>
553
554<h2>Conclusions</h2>
555
556<p>It has been very interesting to see how a lattice-based SNARK works, its machinery and tricks.
557Also, Labrador is of special interest because it was a big step forward on lattice-based SNARKs since it has good proof sizes; asymptotically of <span class="math inline">\(\mathcal{O}(\log n)\)</span>, and for <span class="math inline">\(2^{16}\)</span> R1CS constraints, the paper reports proof sizes of 54 kbytes.</p>
558
559<div style="text-align:center;">
560<a target="_blank" href="img/posts/labrador/proof-sizes-table.png">
561 <img style="width:80%"
562 src="img/posts/labrador/proof-sizes-table.png"></img>
563</a>
564<br>
565<i style="color:#374072">table from the Labrador paper</i>
566</div>
567
568<p><br></p>
569
570<p>An interesting thing in Labrador is the capacity to mix binary and non-binary R1CS constraints, which get reshaped into the <span class="math inline">\(f(s)\)</span> and <span class="math inline">\(f'(s)\)</span> Labrador constraints. This is nice, because for many zk-circuits we want to prove binary-based operations (such as traditional hashes), while doing arithmetic logic, and in Labrador we can mix both in parallel.</p>
571
572<p>Other post-quantum safe SNARK schemes are based on hashes (eg. STARKs), widely used in the industry; but what seems interesting of the lattice-based cryptography is that lattices have more algebraic structure, and while a bit less developed in production than hash based proofs, they have interesting potential.</p>
573
574<p>I’ve enjoyed studying Labrador, and definitely I’ll keep exploring other lattice-based schemes while also going a bit down to the math behind them.</p>
575
576 </div>
577
578 <footer style="text-align:center; margin-top:100px;margin-bottom:50px;">
579 <div class="container">
580 <br>
581 <a href="/blog">Go to main</a>
582 <br><br>
583 <div class="row">
584 <ul class="list-inline">
585 <li><a href="https://twitter.com/arnaucube"
586 style="color:gray;text-decoration:none;"
587 target="_blank">twitter.com/arnaucube</a>
588 </li>
589 <li><a href="https://github.com/arnaucube"
590 style="color:gray;text-decoration:none;"
591 target="_blank">github.com/arnaucube</a>
592 </li>
593 </ul>
594 </div>
595 <div class="row" style="display:inline-block;">
596 Blog made with <a href="http://github.com/arnaucube/blogo/"
597 target="_blank" style="color: gray;text-decoration:none;">Blogo</a>
598 </div>
599 </div>
600 </footer>
601
602 <script>
603 </script>
604 <script src="js/external-links.js"></script>
605 <script>hljs.initHighlightingOnLoad();</script>
606 <script defer src="js/katex/katex.min.js"></script>
607 <script defer src="js/katex/auto-render.min.js"></script>
608 <script>
609 document.addEventListener("DOMContentLoaded", function() {
610 renderMathInElement(document.body, {
611 displayMode: false,
612 // customised options
613 // • auto-render specific keys, e.g.:
614 delimiters: [
615 {left: '$$', right: '$$', display: true},
616 {left: '$', right: '$', display: false},
617 {left: "\\[", right: "\\]", display: true},
618 {left: "\\(", right: "\\)", display: false},
619 {left: "\\begin{equation}", right: "\\end{equation}", display: true}
620 ],
621 // • rendering keys, e.g.:
622 throwOnError : true
623 });
624 });
625
626 ///
627 let theme = localStorage.getItem("theme");
628 if ((theme === "light-theme")||(theme==null)) {
629 theme = "light-theme";
630 document.getElementById("themeSwitcher").checked = false;
631 } else if (theme === "dark-theme") {
632 theme = "dark-theme";
633 document.getElementById("themeSwitcher").checked = true;
634 }
635 document.body.className = theme;
636 localStorage.setItem("theme", theme);
637
638 function switchTheme() {
639 theme = localStorage.getItem("theme");
640 if (theme === "light-theme") {
641 theme = "dark-theme";
642 document.getElementById("themeSwitcher").checked = true;
643 } else {
644 theme = "light-theme";
645 document.getElementById("themeSwitcher").checked = false;
646 }
647 document.body.className = theme;
648 localStorage.setItem("theme", theme);
649
650 console.log(theme);
651 }
652 </script>
653 <script>
654 function tagLinks(tagName) {
655 var tags = document.getElementsByTagName(tagName);
656 for (var i=0, hElem; hElem = tags[i]; i++) {
657 if (hElem.parentNode.className=="row postThumb") {
658 continue;
659 }
660 hElem.id = hElem.innerHTML.toLowerCase().replace(" ", "-");
661 hElem.innerHTML = "<a style='color:black!important;' href='#"+hElem.id+"'>"+hElem.innerHTML+"</a>";
662 }
663 }
664 tagLinks("h2");
665 tagLinks("h3");
666 tagLinks("h4");
667 tagLinks("h5");
668 </script>
669 <script>
670function generateTOC(tocContainerId = "toc") {
671 const tocContainer = document.getElementById(tocContainerId);
672 if (!tocContainer) return;
673
674 const headings = document.querySelectorAll("h2, h3, h4, h5, h6");
675 if (!headings.length) return;
676
677 // Generate IDs if missing
678 headings.forEach((heading, index) => {
679 if (!heading.id) {
680 heading.id =
681 heading.textContent
682 .trim()
683 .toLowerCase()
684 .replace(/[^\w\s-]/g, "")
685 .replace(/\s+/g, "-") +
686 "-" +
687 index;
688 }
689 });
690
691 const toc = document.createElement("ul");
692 let currentLevel = 1;
693 let currentList = toc;
694 const stack = [toc];
695
696 headings.forEach((heading) => {
697 const level = parseInt(heading.tagName.substring(1), 10);
698
699 const li = document.createElement("li");
700 const a = document.createElement("a");
701
702 a.href = "#" + heading.id;
703 a.textContent = heading.textContent;
704
705 li.appendChild(a);
706
707 if (level > currentLevel) {
708 for (let i = currentLevel; i < level; i++) {
709 const nestedList = document.createElement("ul");
710
711 const lastLi =
712 currentList.lastElementChild ||
713 currentList.appendChild(document.createElement("ul"));
714
715 lastLi.appendChild(nestedList);
716
717 stack.push(nestedList);
718 currentList = nestedList;
719 }
720 } else if (level < currentLevel) {
721 for (let i = currentLevel; i > level; i--) {
722 stack.pop();
723 }
724 currentList = stack[stack.length - 1];
725 }
726
727 currentList.appendChild(li);
728 currentLevel = level;
729 });
730
731 tocContainer.innerHTML = "";
732 tocContainer.appendChild(toc);
733}
734
735document.addEventListener("DOMContentLoaded", () => {
736 generateTOC();
737});
738 </script>
739 <script src="js/mermaid.min.js"></script>
740
741 </body>
742</html>
743