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 <link rel="alternate" type="application/rss+xml" title="arnaucube - blog RSS" href="https://arnaucube.com/blog/rss.xml">
38</head>
39
40 <body>
41
42 <!-- o_gradient_background" -->
43 <nav id="mainNav" class="navbar navbar-default navbar-fixed-top"
44 style="height:50px;font-size:100%;">
45 <div class="container">
46 <div style="float:left;">
47 <a href="/blog" style="color:#000;display:inline-block;">blog</a>
48 <span style="margin-right:20px; margin-left:20px;">|</span>
49 <a href="/blog/notes.html" style="font-size:90%;color:#000;display:inline-block;">notes</a>
50 </div>
51 <div style="float:right;">
52 <a href="/" style="color:#000;display:inline-block;margin-right:10px;">arnaucube.com</a>
53 <a href="/blog/rss.xml" target="_blank"
54 type="application/rss+xml" title="subscribe via RSS" aria-label="subscribe via RSS">
55 <img width="12px;" src="img/rss.png" />
56 </a>
57 <div class="onoffswitch" style="margin-left:0px;display:inline-block;" title="change theme">
58 <input onclick="switchTheme()" type="checkbox" name="onoffswitch" class="onoffswitch-checkbox"
59 id="themeSwitcher">
60 <label class="onoffswitch-label" for="themeSwitcher"></label>
61 </div>
62 </div>
63 </div>
64 <!-- <img style="height:5px; width:100%; margin-top:8px;" src="img/gradient-line.jpg" /> -->
65 </nav>
66
67
68
69 <div class="container" style="margin-top:0px;max-width:800px;">
70 <h1>Notes on Labrador, a lattice-based SNARK scheme</h1>
71
72<p><em>2026-06-11</em></p>
73
74<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>
75
76<p>The structure of this post is the following:</p>
77
78<div id="toc"></div>
79
80<h2>Notation</h2>
81
82<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>
83
84<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>
85
86<h2>A bit of background on lattices</h2>
87
88<h3>Lattices intro</h3>
89
90<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>
91<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>
92
93<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>
94
95<p><br></p>
96
97<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>
98
99<div style="text-align:center;">
100<img style="width:70%"
101src="img/posts/labrador/lattice-spherepackingproblem.png"></img>
102<br>
103<i></i>
104</div>
105
106<h3>MSIS problem</h3>
107
108<p><em>MSIS</em> problem stands for <em>Module Short Integer Solution</em> problem, and it is as follows:</p>
109
110<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>
111<p><span class="math display">\[A \cdot z = \sum_i a_i \cdot z_i = 0 \in R_q^n\]</span></p>
112<blockquote>
113<p><em>Remarks:</em></p>
114
115<ul>
116<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>
117<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>
118<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>
119</ul>
120</blockquote>
121
122<p>So overall when doing lattice-based cryptography, we will be interested into keeping the values <em>short</em>, aka. of small norm.</p>
123
124<p>Specifically, Labrador relies on the hardness of finding short solutions to linear equations over polynomial rings.</p>
125
126<p><br></p>
127
128<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>
129
130<h3>Ajtai commitments</h3>
131
132<p>We use a variant of the Ajtai commitments, where the messages are ring elements with small norms.</p>
133
134<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>
135
136<p>In other words, Ajtai commitments are essentially MSIS instances.</p>
137
138<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>
139
140<h2>Labrador constraints</h2>
141
142<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>
143
144<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>
145
146<p>While in other SNARK systems we worked with constraints in the shape of R1CS or Plonkish, LaBRADOR defines its constraints as</p>
147<p><span class="math display">\[\boxed{
148f(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
149}
150\]</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>
151
152<p>There are two different families of constraints, which are evaluated differently:</p>
153
154<ul>
155<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>
156<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>
157</ul>
158
159<p>To avoid future doubts, let’s write down what are some constant values:</p>
160
161<ul>
162<li><span class="math inline">\(r\)</span>: amount of witness vectors <span class="math inline">\(s_1, \ldots, s_r\)</span></li>
163<li><span class="math inline">\(K = |\mathcal{F}|\)</span>: amount of original constraints of fully vanishing dot products</li>
164<li><span class="math inline">\(L = |\mathcal{F}~'|\)</span>: amount of original constraints where the constant term is zero</li>
165</ul>
166
167<!--
168(HIDDEN)
169> *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$.
170>
171> 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)).
172-->
173
174<h2>Protocol</h2>
175
176<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>
177
178<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>
179<p><span class="math display">\[
180f(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
181\]</span></p><p><span class="math display">\[
182f'(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
183\]</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>
184
185<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>
186
187<div style="text-align:center;">
188<img style="width:60%"
189src="img/posts/labrador/constraint-polynomials-evolution.jpg"></img>
190<br>
191<i style="color:#374072">$f(s), f'(s)$ are original polynomials, from the mentioned families $\mathcal{F}$ and $\mathcal{F}~'$ respectively,<br>
192$f_{proj}(s), f''(s)$, $F(s)$ are polynomials that we will describe in the following sections.</i>
193</div>
194
195<p><br>
196Labrador reduces proof size through four transformations unfolded over the next sections:</p>
197
198<ol>
199<li>Commit to the witness</li>
200<li>Reduce norm checking with Johnson-Lindenstrauss projections</li>
201<li>Aggregate many constraints into one</li>
202<li>Amortize openings</li>
203<li>Recurse</li>
204</ol>
205
206<h3>1. Committing to the witness</h3>
207
208<p>We name <em>inner commitments</em> the commitments to the original witness. Those commitments are</p>
209<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>
210<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>
211
212<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>
213
214<p>The commitment to the original commitment, is named <em>outer commitment</em>, and it is computed as</p>
215<p><span class="math display">\[u_1 = B \cdot t\]</span></p><p>that is</p>
216<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>
217
218<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>
219
220<h3>The σ₋₁ trick</h3>
221
222<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>
223
224<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>
225
226<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>
227
228<p>Notice that in Labrador, vectors are encoded as polynomials in <span class="math inline">\(R_q\)</span>, ie</p>
229<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>
230<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>
231
232<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>
233
234<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>
235
236<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>
237
238<p>Then, when multiplying</p>
239<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>
240
241<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>
242
243<h3>2. Johnson-Lindenstrauss projection</h3>
244
245<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>
246
247<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>
248
249<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>
250
251<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>
252
253<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>
254<p><span class="math display">\[
255f'(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
256\]</span></p><p>And the projection constraints, which encode the check for the J-L projection in the Labrador constraints shape:</p>
257
258<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>
259<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>
260<p><span class="math display">\[
261f_{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
262\]</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>
263
264<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>
265
266<h3>3. Aggregation steps</h3>
267
268<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>
269
270<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>
271
272<h4>3.1. 1st aggregation</h4>
273
274<p>The prover linearly combines</p>
275
276<ul>
277<li>the <span class="math inline">\(L\)</span> original constraints from <span class="math inline">\(f'(s)\)</span></li>
278<li>the <span class="math inline">\(256\)</span> constraints that prove the Johnson-Lindenstrauss projection, <span class="math inline">\(f_{proj}(s)\)</span></li>
279</ul>
280
281<p>as follows</p>
282<p><span class="math display">\[
283f''^{(k)}(s) =
284\sum_{l=1}^L \psi_l^{(k)} \cdot f'^{(l)}(s)
285+
286\sum_{j=1}^{256} w_j^{(k)} \cdot f_{proj}(s)
287=
288\\
289= \underbrace{ \sum_{l=1}^L \psi_l^{(k)} \cdot f'^{(l)}(s) }_{(i.)~ \text{lin.comb. of the original constraints}}
290+
291\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}}
292\]</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>
293<p><span class="math display">\[
294(i.):~
295\sum_l \psi_l^{(k)} \cdot f'^{(l)}(s) =
296\sum_l \psi_l^{(k)} \cdot \left(
297 \sum_{i,j} a_{ij}^{'(l)} \cdot \langle s_i, s_j \rangle
298 + \sum_i \langle \phi_i^{'(l)}, s_i \rangle - b_0^{'(k)}
299\right)\\
300=
301\underbrace{
302\sum_{i,j} \left( \sum_l \psi_l^{(k)} \cdot a_{ij}^{'(l)} \right) \cdot \langle s_i, s_j \rangle
303}_{(i.A)}
304\underbrace{
305+ \sum_i \left( \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)} \right) \cdot s_i
306- \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
307}_{(i.B)}
308\]</span></p><p>For the <span class="math inline">\((i.A)\)</span> part, we can set</p>
309<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>
310<p><span class="math display">\[
311(i.A):~
312 \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
313\]</span></p><p>Now tackle <span class="math inline">\((ii.)\)</span>:</p>
314<p><span class="math display">\[
315(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
316- \sum_j w_j^{(k)} \cdot p_j
317\]</span></p><p>Now let’s put together <span class="math inline">\((i.B)\)</span> and <span class="math inline">\((ii)\)</span>:</p>
318<p><span class="math display">\[
319\overbrace{
320 \textcolor{green}{
321 \sum_i ( \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)} ) \cdot s_i
322 }
323 \textcolor{blue}{
324 - \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
325 }
326}^{(i.B)}
327+
328\overbrace{
329 \textcolor{orange}{
330 \sum_i \langle \sum_j w_j^{(k)} \sigma_{-1}(\pi_i^{(j)}),~ s_i \rangle
331 }
332 \textcolor{red}{
333 - \sum_j w_j^{(k)} \cdot p_j
334 }
335}^{(ii.)}
336=\\~\\
337=
338 \sum_i
339\textcolor{green}{
340 \big\langle
341 \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)}
342 }
343 +
344 \textcolor{orange}{
345 \sum_l w_j^{(k)} \cdot \sigma_{-1}(\pi_i^{(j)}), s_i
346 \big\rangle
347 }
348 +
349 \textcolor{blue}{
350 \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
351 }
352 +
353 \textcolor{red}{
354 \sum_j w_j^{(k)} \cdot p_j
355 }
356\]</span></p><p>without colors:</p>
357<p><span class="math display">\[
358=
359\sum_i
360 \big\langle
361 \underbrace{
362 \sum_l \psi_l^{(k)} \cdot \phi_i^{'(l)}
363 +
364 \sum_l w_j^{(k)} \cdot \sigma_{-1}(\pi_i^{(j)})
365 }_{\phi_i^{''(k)}},
366 s_i
367 \big\rangle
368 +
369 \underbrace{
370 \sum_l \psi_l^{(k)} \cdot b_0^{'(l)}
371 +
372 \sum_j w_j^{(k)} \cdot p_j
373 }_{b_0^{''(k)} ~\text{(constant term)}}
374 \\
375 =
376 \sum_{i=1}^r \langle \textcolor{blue}{\phi_i^{''(k)}}, s_i \rangle - \textcolor{orange}{b_0^{''(k)}}
377\]</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>
378<p><span class="math display">\[
379\boxed{
380f''^{(k)}(s) =
381\overbrace{
382\sum_{i,j=1}^r \textcolor{magenta}{a_{ij}^{''(k)}} \cdot \langle s_i, s_j \rangle
383}^{(i.A)}
384+
385\overbrace{
386\sum_{i=1}^r \langle \textcolor{blue}{\phi_i^{''(k)}}, s_i \rangle - \textcolor{orange}{b_0^{''(k)}}
387}^{(i.B) + (ii.)}
388}
389\]</span></p><p>such that <span class="math inline">\(ct(f''^{(k)}(s)) = 0\)</span>.</p>
390
391<p><br></p>
392
393<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>
394
395<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>
396
397<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>
398
399<p><br></p>
400
401<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>
402<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>
403<h4>3.2. 2nd aggregation</h4>
404
405<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>
406
407<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>
408
409<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>
410
411<p>Then the prover will compute</p>
412<p><span class="math display">\[
413F(s) = \sum_{k=1}^K \alpha_k \cdot f^{(k)}(s) + \sum_{k=1}^{\lceil 128/ \log q \rceil} \beta_k \cdot f''^{(k)}\\
414=
415\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)
416+
417\sum_{k=1}^{\lceil 128/ \log q \rceil} \beta_k \cdot
418\left(
419 \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)}
420\right)
421\]</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>
422<p><span class="math display">\[
423= \sum_{i,j=1}^r
424\underbrace{
425 \left( \sum_{k=1}^K \alpha_k a_{ij}^{(k)}
426 +
427 \sum_{k=1}^{\lceil 128/\log q \rceil} \beta_k a_{ij}''^{(k)}
428 \right)
429}_{a_{ij}}
430\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
431\\
432- \underbrace{ \left( \sum_{k=1}^K \alpha_k b^{(k)} + \sum_{k=1}^{\lceil 128/\log q \rceil} \beta_k b''^{(k)} \right) }_{b}
433\]</span></p><p><span class="math display">\[
434\boxed{
435 F(s) = \sum_{i,j} a_{ij} \langle s_i, s_j \rangle + \sum_i \langle \phi_i, s_i \rangle - b
436}
437\]</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>
438
439<h3>4. Amortization</h3>
440
441<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>
442<p><span class="math display">\[z = \sum_{i=1}^r c_i \cdot s_i\]</span></p><p>and its respective committed version</p>
443<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>
444
445<p>Then the verifier checks</p>
446<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>
447<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>
448
449<p><br></p>
450
451<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>
452
453<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>
454
455<p>Let the <em>garbage polynomials</em> be</p>
456<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>
457
458<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>
459
460<blockquote>
461<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>
462
463<p>The conceptual explanation describes the second outer commitment <span class="math inline">\(u_2\)</span> as</p>
464<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>
465<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>
466</blockquote>
467
468<p>Then, the verifier will do the following checks:</p>
469<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>
470
471<h3>5. Recursion</h3>
472
473<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>
474
475<p>The idea now, is to recurse, encoding the protocol checks into new Labrador constraints, and then performing again the protocol.</p>
476
477<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>
478<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>
479
480<p>Then, the quadratic dot product becomes</p>
481<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>
482
483<p>Write the vectors <span class="math inline">\(z^{(0)}, z^{(1)}, v\)</span> as concatenations of vectors:</p>
484<p><span class="math display">\[
485z^{(0)} = s_1 || s_2 || \ldots || s_{\nu}\\
486z^{(1)} = s_{\nu+1} || \ldots || s_{2\nu}\\
487v = s_{2\nu+1} || \ldots || s_{2\nu+ \mu}
488\]</span></p><p>that is <span class="math inline">\(r' = 2 \nu + \mu\)</span> vectors in total.</p>
489
490<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>
491
492<h4>encoding check (i.)</h4>
493
494<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>
495<p><span class="math display">\[
496\langle z, z \rangle = \langle z^{(0)} + b z^{(1)}, z^{(0)} + b z^{(1)} \rangle\\
497= \langle z^{(0)}, z^{(0)} \rangle + 2b \langle z^{(0)}, z^{(1)} \rangle + b^2 \langle z^{(1)}, z^{(1)} \rangle
498\]</span></p><p>that is, three separate dot products. Then we place</p>
499<p><span class="math display">\[
500z^{(0)} ~\text{into}~ s_1', \ldots, s'_{\nu}\\
501z^{(1)} ~\text{into}~ s_{\nu+1}', \ldots, s'_{2\nu}
502\]</span></p><p>so that</p>
503<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>
504<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>
505<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>
506
507<ul>
508<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>
509<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>
510<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>
511</ul>
512
513<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>
514
515<h4>encoding check (ii.)</h4>
516
517<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>
518<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>
519<p><span class="math display">\[
520z^{(0)} = s_1 || s_2 || \ldots || s_{\nu}\\
521z^{(1)} = s_{\nu+1} || \ldots || s_{2\nu}\\
522v = s_{2\nu+1} || \ldots || s_{2\nu+ \mu}
523\]</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>
524
525<ul>
526<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>
527<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>
528<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>
529</ul>
530
531<h4>encoding check (iii.)</h4>
532
533<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>
534
535<p>With this, we can encode the checks <span class="math inline">\((i.),~ (ii.),~ (iii.)\)</span> into the Labraddor constraint shape</p>
536<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>
537
538<h4>encoding commitments checks</h4>
539
540<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>
541<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>
542
543<p><br></p>
544
545<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>
546<p><span class="math display">\[
547u_1 = B \cdot t + C \cdot g\\
548u_2 = D \cdot h
549\]</span></p><p>which we can encode as</p>
550<p><span class="math display">\[
551\langle B_{row}, t \rangle + \langle C_{row}, g \rangle = (u_1)_{row}\\
552\langle D_{row}, h \rangle = (u_2)_{row}
553\]</span></p><p>which, as before, we can also reshape into the dot product Labrador constraints.</p>
554
555<p><br></p>
556
557<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>
558
559<h2>Conclusions</h2>
560
561<p>It has been very interesting to see how a lattice-based SNARK works, its machinery and tricks.
562Also, 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>
563
564<div style="text-align:center;">
565<a target="_blank" href="img/posts/labrador/proof-sizes-table.png">
566 <img style="width:80%"
567 src="img/posts/labrador/proof-sizes-table.png"></img>
568</a>
569<br>
570<i style="color:#374072">table from the Labrador paper</i>
571</div>
572
573<p><br></p>
574
575<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>
576
577<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>
578
579<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>
580
581 </div>
582
583 <footer style="text-align:center; margin-top:100px;margin-bottom:50px;">
584 <div class="container">
585 <br>
586 <a href="/blog">Go to main</a>
587 <br><br>
588 <div class="row">
589 <ul class="list-inline">
590 <li><a href="https://twitter.com/arnaucube"
591 style="color:gray;text-decoration:none;"
592 target="_blank">twitter.com/arnaucube</a>
593 </li>
594 <li><a href="https://github.com/arnaucube"
595 style="color:gray;text-decoration:none;"
596 target="_blank">github.com/arnaucube</a>
597 </li>
598 </ul>
599 </div>
600 <div class="row" style="display:inline-block;">
601 Blog made with <a href="http://github.com/arnaucube/blogo/"
602 target="_blank" style="color: gray;text-decoration:none;">Blogo</a>
603 </div>
604 </div>
605 </footer>
606
607 <script>
608 </script>
609 <script src="js/external-links.js"></script>
610 <script>hljs.initHighlightingOnLoad();</script>
611 <script defer src="js/katex/katex.min.js"></script>
612 <script defer src="js/katex/auto-render.min.js"></script>
613 <script>
614 document.addEventListener("DOMContentLoaded", function() {
615 renderMathInElement(document.body, {
616 displayMode: false,
617 // customised options
618 // • auto-render specific keys, e.g.:
619 delimiters: [
620 {left: '$$', right: '$$', display: true},
621 {left: '$', right: '$', display: false},
622 {left: "\\[", right: "\\]", display: true},
623 {left: "\\(", right: "\\)", display: false},
624 {left: "\\begin{equation}", right: "\\end{equation}", display: true}
625 ],
626 // • rendering keys, e.g.:
627 throwOnError : true
628 });
629 });
630
631 ///
632 let theme = localStorage.getItem("theme");
633 if ((theme === "light-theme")||(theme==null)) {
634 theme = "light-theme";
635 document.getElementById("themeSwitcher").checked = false;
636 } else if (theme === "dark-theme") {
637 theme = "dark-theme";
638 document.getElementById("themeSwitcher").checked = true;
639 }
640 document.body.className = theme;
641 localStorage.setItem("theme", theme);
642
643 function switchTheme() {
644 theme = localStorage.getItem("theme");
645 if (theme === "light-theme") {
646 theme = "dark-theme";
647 document.getElementById("themeSwitcher").checked = true;
648 } else {
649 theme = "light-theme";
650 document.getElementById("themeSwitcher").checked = false;
651 }
652 document.body.className = theme;
653 localStorage.setItem("theme", theme);
654
655 console.log(theme);
656 }
657 </script>
658 <script>
659 function tagLinks(tagName) {
660 var tags = document.getElementsByTagName(tagName);
661 for (var i=0, hElem; hElem = tags[i]; i++) {
662 if (hElem.parentNode.className=="row postThumb") {
663 continue;
664 }
665 hElem.id = hElem.innerHTML.toLowerCase().replace(" ", "-");
666 hElem.innerHTML = "<a style='color:black!important;' href='#"+hElem.id+"'>"+hElem.innerHTML+"</a>";
667 }
668 }
669 tagLinks("h2");
670 tagLinks("h3");
671 tagLinks("h4");
672 tagLinks("h5");
673 </script>
674 <script>
675function generateTOC(tocContainerId = "toc") {
676 const tocContainer = document.getElementById(tocContainerId);
677 if (!tocContainer) return;
678
679 const headings = document.querySelectorAll("h2, h3, h4, h5, h6");
680 if (!headings.length) return;
681
682 // Generate IDs if missing
683 headings.forEach((heading, index) => {
684 if (!heading.id) {
685 heading.id =
686 heading.textContent
687 .trim()
688 .toLowerCase()
689 .replace(/[^\w\s-]/g, "")
690 .replace(/\s+/g, "-") +
691 "-" +
692 index;
693 }
694 });
695
696 const toc = document.createElement("ul");
697 let currentLevel = 1;
698 let currentList = toc;
699 const stack = [toc];
700
701 headings.forEach((heading) => {
702 const level = parseInt(heading.tagName.substring(1), 10);
703
704 const li = document.createElement("li");
705 const a = document.createElement("a");
706
707 a.href = "#" + heading.id;
708 a.textContent = heading.textContent;
709
710 li.appendChild(a);
711
712 if (level > currentLevel) {
713 for (let i = currentLevel; i < level; i++) {
714 const nestedList = document.createElement("ul");
715
716 const lastLi =
717 currentList.lastElementChild ||
718 currentList.appendChild(document.createElement("ul"));
719
720 lastLi.appendChild(nestedList);
721
722 stack.push(nestedList);
723 currentList = nestedList;
724 }
725 } else if (level < currentLevel) {
726 for (let i = currentLevel; i > level; i--) {
727 stack.pop();
728 }
729 currentList = stack[stack.length - 1];
730 }
731
732 currentList.appendChild(li);
733 currentLevel = level;
734 });
735
736 tocContainer.innerHTML = "";
737 tocContainer.appendChild(toc);
738}
739
740document.addEventListener("DOMContentLoaded", () => {
741 generateTOC();
742});
743 </script>
744 <script src="js/mermaid.min.js"></script>
745
746 </body>
747</html>
748