math/pinocchio-groth16.tex
pinocchio-groth16.texRaw
1\documentclass{article}
2\usepackage[utf8]{inputenc}
3\usepackage{amsfonts}
4\usepackage{amsthm}
5\usepackage{amsmath}
6\usepackage{enumerate}
7\usepackage{hyperref}
8\usepackage{amssymb}
9\usepackage{tikz} % diagram
10
11\begin{filecontents}[overwrite]{pinocchio-groth16.bib}
12@misc{cryptoeprint:2013/279,
13 author = {Bryan Parno and Craig Gentry and Jon Howell and Mariana Raykova},
14 title = {Pinocchio: Nearly Practical Verifiable Computation},
15 howpublished = {Cryptology {ePrint} Archive, Paper 2013/279},
16 year = {2013},
17 url = {https://eprint.iacr.org/2013/279}
18}
19@misc{cryptoeprint:2016/260,
20 author = {Jens Groth},
21 title = {On the Size of Pairing-based Non-interactive Arguments},
22 howpublished = {Cryptology {ePrint} Archive, Paper 2016/260},
23 year = {2016},
24 url = {https://eprint.iacr.org/2016/260}
25}
26
27@misc{pairings,
28 note = {\url{https://github.com/arnaucube/math/blob/master/weil-pairing.pdf}},
29 url = {https://github.com/arnaucube/math/blob/master/weil-pairing.pdf}
30}
31\end{filecontents}
32\nocite{*} % TODO review
33
34
35\newtheorem{thm}{Theorem}[section]
36\newtheorem{lemma}[thm]{Lemma}
37\newtheorem{prop}[thm]{Proposition}
38\newtheorem{cor}[thm]{Corollary}
39\newtheorem{defn}[thm]{Definition}
40
41
42\title{Pinocchio and Groth16 notes}
43\author{arnaucube}
44\date{2026}
45
46\begin{document}
47
48\maketitle
49
50\begin{abstract}
51 Notes taken while studying the schemes Pinocchio (\cite{cryptoeprint:2013/279}) and Groth16 (\cite{cryptoeprint:2016/260}).
52
53 Usually while reading books and papers I take handwritten notes in a notebook, this document contains some of them re-written to $LaTeX$.
54
55 The proofs may slightly differ from the ones from the books or papers, since I try to extend them for a deeper understanding.
56\end{abstract}
57
58\tableofcontents
59\newpage
60
61
62\section{Introduction}
63
64% TODO.
65% what we want to prove, how it connects with R1CS & QAP
66
67
68\section{R1CS}
69% TODO Add R_{R1CS} relation definition.
70
71Rank-One Constraint System (R1CS) is the representation of the constraints of the circuit by 3 linear combinations, where there is one constraint per operation.
72
73$$
74\begin{aligned}
75(a_{11}w_1 + a_{12}w_2 + ... + a_{1n}w_n) \cdot (b_{11}w_1 + b_{12}w_2 + ... + b_{1n}w_n)\\- (c_{11}w_1 + c_{12}w_2 + ... + c_{1n}w_n) = 0
76\\
77(a_{21}w_1 + a_{22}w_2 + ... + a_{2n}w_n) \cdot (b_{21}w_1 + b_{22}w_2 + ... + b_{2n}w_n)\\- (c_{21}w_1 + c_{22}w_2 + ... + c_{2n}w_n) = 0
78\\
79(a_{31}w_1 + a_{32}w_2 + ... + a_{3n}w_n) \cdot (b_{31}w_1 + b_{32}w_2 + ... + b_{3n}w_n)\\- (c_{31}w_1 + c_{32}w_2 + ... + c_{3n}w_n) = 0
80\\
81\ldots
82\\
83(a_{m1}w_1 + a_{m2}w_2 + ... + a_{mn}w_n) \cdot (b_{m1}w_1 + b_{m2}w_2 + ... + b_{mn}w_n)\\- (c_{m1}w_1 + c_{m2}w_2 + ... + c_{mn}w_n) = 0
84\end{aligned}
85$$
86
87Where the R1CS linear combinations can be represented by three matrices $A$, $B$ and $C$:
88$$
89\begin{aligned}
90A =
91\begin{pmatrix}
92a_{11} & a_{12} & ... & a_{1n}\\
93a_{21} & a_{22} & ... & a_{2n}\\
94a_{31} & a_{32} & ... & a_{3n}\\
95...\\
96a_{m1} & a_{m2} & ... & a_{mn}
97\end{pmatrix}
98B =
99\begin{pmatrix}
100b_{11} & b_{12} & ... & b_{1n}\\
101b_{21} & b_{22} & ... & b_{2n}\\
102b_{31} & b_{32} & ... & b_{3n}\\
103...\\
104b_{m1} & b_{m2} & ... & b_{mn}
105\end{pmatrix}
106\\
107C =
108\begin{pmatrix}
109c_{11} & c_{12} & ... & c_{1n}\\
110c_{21} & c_{22} & ... & c_{2n}\\
111c_{31} & c_{32} & ... & c_{3n}\\
112...\\
113c_{m1} & c_{m2} & ... & c_{mn}
114\end{pmatrix}
115\end{aligned}
116$$
117
118Where
119$(A, B, C) = A w \circ B w - C w = 0$
120
121The process that converts the \emph{flat constraints} into \emph{R1CS} is the following:
122
123Lets assume that we have a constraint $5 w_3 = w_1 \cdot 2 w_2$ (being $w_1$, $w_2$ and $w_3$ the signals 1, 2 and 3 respectively)). We can represent this constraint in the matrices form by:
124
125$$
126\begin{aligned}
127A =
128\begin{pmatrix}
1291 & 0 & 0 & ... & 0\\
130\end{pmatrix}
131\\
132B =
133\begin{pmatrix}
1340 & 2 & 0 & ... & 0\\
135\end{pmatrix}
136\\
137C =
138\begin{pmatrix}
1390 & 0 & 5 & ... & 0\\
140\end{pmatrix}
141\end{aligned}
142$$
143
144
145Which in the R1CS equation form would look as:
146$$
147\begin{aligned}
148(1 \cdot w_1 + 0 \cdot w_2 + 0 \cdot w_3 + ... + 0 \cdot w_n) \cdot
149(0 \cdot w_1 + 2 \cdot w_2 + 0 \cdot w_3 + ... + 0 \cdot w_n) -\\
150(0 \cdot w_1 + 0 \cdot w_2 + 5 \cdot w_3 + ... + 0 \cdot w_n) = 0
151\end{aligned}
152$$
153
154If we simplify the previous liniar combination we get:
155$$
156\begin{aligned}
157(1 \cdot w_1) \cdot (2 \cdot w_2) - (5 \cdot w_3) = 0
158\\
159w_1 \cdot 2w_1 - 5 w_3 = 0
160\\
1615 w_3 = w_1 \cdot 2w_1
162\end{aligned}
163$$
164Where $5 w_3 = w_1 \cdot 2w_1$ is the constraint that we wanted to represent in the R1CS format.
165
166The nice thing from R1CS is that allows us to standarize the constraints in an equation fashion, where all the signals are involved and we 'activate' these ones that are used in each constraint.
167Since we have now the constraints in a polynomial format, we can do work with it in the polynomial way.
168
169
170\section{QAP (Quadratic Arithmetic Programs)} \label{qap}
171
172Once we have the constraints of a circuit represented in \emph{R1CS}, we can do one more iteration and represent it in \emph{Quadratic Arithmetic Programs (QAP)}.
173%% TODO %%
174\emph{QAP} is a representation of the XXX in a linear combination of the \emph{R1CS}, represented by 3 polynomials $a(X)$, $b(X)$ and $c(X)$.
175The \emph{QAP} consists of the 3 polynomials $a(X)$, $b(X)$ and $c(X)$, plus a divisor polynomial $h(X) \in \mathbb{F}[X]^{<d}$.
176
177The main idea behind the \emph{QAP} is that they 'contain' all the constraints of the circuit, meaning that these polynomials need to be able to generate all the constraints.
178
179In order to 'collapse' the \emph{R1CS} polynomials into the 3 polynomials of the \emph{QAP}, we make use of \emph{polynomial interpolation}, also named \emph{Lagrange interpolation}. \emph{Lagrange interpolation} allows for a group of points, to find the smallest degree and unique polynomial that goes through all those points. It can be calculated by computing:
180
181$$L(X) = \sum_{j=0}^{n} y_j l_j(X)$$
182
183where $l_j(X)$ is:
184$$
185l_j(X) = \prod_{0\leq m \leq k ; m\neq j}
186\frac{X-x_m}{x_j - x_m}
187...
188\frac{(X-x_{j-1})}{(x_j - x_{j-1})}
189\frac{(X-x_{j+1})}{(x_j - x_{j+1})}
190...
191\frac{X-x_k}{x_j - x_k}
192$$
193
194The intuition behind the \emph{Lagrange interpolation} is quite simple. If we have two points (on a 2 dimensional plane) we can find a line that goes through both points (this can be done with a pen and a ruler on a paper), if we have 3 points we can find a curved line that goes through all the three points, if we do this through math trying to get the lowest degree curve we obtain a 2nd degree polynomial. This can be generalized using the *Lagrange interpolation*, allowing us for a group of $n$ points to find a $n-1$ degree polynomial that goes through all of them.
195
196In our case, \emph{Lagrange interpolation} is used to go from the \emph{R1CS} polynomials into the \emph{QAP} polynomials, which are defined by:
197
198$$
199\begin{aligned}
200 a(X) = (\alpha_1(X)w_1 + \alpha_2(X)w_2 + ... + \alpha_n(X)w_n) = \sum_{i=1}^n \alpha_i(X) w_i\\
201 b(X) = (\beta_1(X)w_1 + \beta_2(X)w_2 + ... + \beta_n(X)w_n) = \sum_{i=1}^n \beta_i(X) w_i\\
202 c(X) = (\gamma_1(X)w_1 + \gamma_2(X)w_2 + ... + \gamma_n(X)w_n) = \sum_{i=1}^n \gamma_i(X) w_i
203\end{aligned}
204$$
205
206The polynomials $a(X), b(X), c(X)$ are the QAP, such that
207$$a(X) \cdot b(X) = c(X)$$
208so that
209$$p(X) = a(X) \cdot b(X) - c(X) = 0$$
210
211that is,
212$$
213\begin{aligned}
214p(X) = (\alpha_1(X)w_1 + \alpha_2(X)w_2 + ... + \alpha_n(X)w_n)
215\\ \cdot (\beta_1(X)w_1 + \beta_2(X)w_2 + ... + \beta_n(X)w_n)
216\\ - (\gamma_1(X)w_1 + \gamma_2(X)w_2 + ... + \gamma_n(X)w_n)
217\\
218= (\sum_{i=1}^n \alpha_i(X) w_i) \cdot (\sum_{i=1}^n \beta_i(X) w_i) - (\sum_{i=1}^n \gamma_i(X) w_i)
219\end{aligned}
220$$
221
222The main idea, is that $p(X)$ defines the constraints of our circuit, so that for a valid witness evaluated at $p(X)$, it will be equal to zero.
223
224
225\vspace{0.5cm}
226
227\section{QAP Relation}
228
229Want to ensure that
230$$
231(\sum_{i=1}^n \alpha_i(X) w_i) \cdot (\sum_{i=1}^n \beta_i(X) w_i) - (\sum_{i=1}^n \gamma_i(X) w_i) = 0
232$$
233
234for a given witness $(w_1, \ldots, w_n) \in \mathbb{F}^n$, which we divide between public inputs and private inputs:
235\begin{align*}
236 \text{public inputs:}~~ \phi &= (w_1, \ldots, w_l) \in \mathbb{F}^l, \\
237 \text{private inputs:}~~ w &= (w_{l+1}, \ldots, w_n) \in \mathbb{F}^{n-l},
238\end{align*}
239
240We denote the relation
241
242$$
243R =
244\left\{
245\begin{aligned}
246(\phi, w) \ \big| \;&
247\phi = (w_1, \ldots, w_l) \in \mathbb{F}^l,\\
248& w = (w_{l+1}, \ldots, w_n) \in \mathbb{F}^{n-l},\\
249& (\sum_{i=1}^n \alpha_i(X) w_i) \cdot (\sum_{i=1}^n \beta_i(X) w_i)
250\equiv
251\sum_{i=1}^{n} \gamma_i(X) w_i
252~\bmod Z(X)
253\end{aligned}
254\right.
255$$
256
257Set
258$$a(X) = \sum_{i=1}^n \alpha_i(X) w_i,~~~~ b(X) = \sum_{i=1}^n \beta_i(X) w_i),~~~~ c(X) = \sum_{i=1}^{n} \gamma_i(X) w_i$$
259
260so that
261$$a(X) \cdot b(X) \equiv c(X) \bmod Z(X)$$
262
263which means that we can prove that
264$$\exists~ h(X) \in \mathbb{F}[X]^{<d}~~ \text{s.th.}~
265a(X) \cdot b(X) - c(X) = h(X) \cdot X(X)$$
266
267
268\section{Simplified protocol}
269Protocol to prove $a(X)b(X)-c(X)=0$.
270
271\paragraph{Setup.}
272The protocol requires a secret random value, which it is encrypted over the elliptic curve group. That is, for given $g_1 \in \mathbb{G}_1$ and $g_2 \in \mathbb{G}_2$ generators of curves $\mathbb{G}_1$ and $\mathbb{G}_2$ respectively, set $[\tau]_1 = g_1^\tau$ and $[\tau]_2 =g_2^\tau$.
273
274$$\{ [\tau^i]_1 \}_0^n = ( [\tau^0]_1, [\tau^1]_1, [\tau^2]_1, \ldots, [\tau^{n-1}]_1)$$
275$$\{ [\tau^i]_2 \}_0^n = ( [\tau^0]_2, [\tau^1]_2, [\tau^2]_2, \ldots, [\tau^{n-1}]_2)$$
276
277\paragraph{Prover.}
278\begin{enumerate}[i.]
279 \item commit to $a(X), b(X), c(X) \in \mathbb{F}[X]$
280
281 $$cm(a) = [a(\tau)]_1 = \sum_{i=0}^{\delta a} a_i \cdot [\tau^i]_1 \in \mathbb{G}_1$$
282
283 notice that it is equal to $\sum a_i \cdot g_1^{\tau^i}$ without knowing $\tau$.
284
285 Same is done for $b(X)$ and $c(X)$:
286 $$cm(b) = [b(\tau)]_2 = \sum_{i=0}^{\delta b} b_i \cdot [\tau^i]_2 \in \mathbb{G}_2$$
287 $$cm(c) = [c(\tau)]_1 = \sum_{i=0}^{\delta c} c_i \cdot [\tau^i]_1 \in \mathbb{G}_1$$
288
289
290 For a challenge $z \in^R \mathbb{F}$, set by the verifier, open the commitments:
291
292 $$q_a(X) = \frac{a(X) - a(z)}{X-z}$$
293
294 Since $a(X)-\underbrace{a(z)}_{=y}$ should be zero at $X-z$, so $a(X) - a(z)$ has a root at $z$, hence it is divisible by $(X-z)$, therefore,
295 $$\exists ~q_a(X) ~~\text{such that}~ a(X)-a(z) = (X-z) \cdot q_a(X)$$
296 therefore
297 $$q_a(X) = \frac{a(X)-a(z)}{X-z}$$
298
299 Same is done for $b(X)$ and $c(X)$,
300 $$q_b(X) = \frac{b(X)-b(z)}{X-z}$$
301 $$q_c(X) = \frac{c(X)-c(z)}{X-z}$$
302
303 And then, evaluate them at the encrypted $\tau$:
304 $$[q_a(\tau)]_1 = \sum_{i=0}^{\delta q_a} q_{a_i} \cdot [\tau^i]_1 \in \mathbb{G}_1$$
305 similarly for $[q_b(\tau)]_2 \in \mathbb{G}_2$ and $[q_c(\tau)]_1 \in \mathbb{G}_1$.
306
307 \item for the relation that we want to prove, $a(X) \cdot b(X) - c(X)=0$,
308 $$\exists~ q(X) \in \mathbb{F}[X] ~~\text{s.th.}~~ a(X)b(X)-c(X)=q(X) \cdot z(X)$$
309 So the prover computes
310 $$q(X) = \frac{a(X) \cdot b(X) - c(X)}{z(X)}$$
311 and it's encrypted evaluation
312 $$[q(\tau)]_1 = \sum_{i=0}^{\delta q} q_i \cdot [\tau^i]_1 \in \mathbb{G}_1$$
313\end{enumerate}
314
315\paragraph{Verifier.}
316\begin{enumerate}[i.]
317 \item verify the commitments:\\
318 The prover has sent the commitments $[a(\tau)]_1,~ [b(\tau)]_2,~ [c(\tau)]_1$, and their respective evaluations at the challenge $z \in \mathbb{F}$: $a(z), b(z), c(z) \in \mathbb{F}$; together with their respective opening proofs: $[q_a(\tau)]_1, [q_b(\tau)]_2, [q_c(\tau)]_1$
319
320 For each commitment, the verifier checks:
321 $$e([q_a(\tau)]_1, [\tau]_2 - [z]_2) \stackrel{?}{=} e([a(\tau)]_1 - [a(z)]_1, [1]_2)$$
322 which is a way of checking the existence of $q_a(X)$ such that $q_a(X) \cdot (X-z) = a(X) - a(z)$.
323
324 If the checks passes, it means that $q_a \in \mathbb{F}[X]$ exists, and thus $a(X) - a(z)$ is divisible ("vanishes") at $(X-z)$, hence $a(X) - a(z)$ has a root at $z$.
325
326 Same is done for $b(X)$ and $c(X)$ commitments:
327 $$e([\tau]_1 - [z]_2, [q_b(\tau)]_1) \stackrel{?}{=} e([1]_1, [b(\tau)]_1 - [b(z)]_1)$$
328 $$e([q_c(\tau)]_1, [\tau]_2 - [z]_2) \stackrel{?}{=} e([c(\tau)]_1 - [c(z)]_1, [1]_2)$$
329
330 \item check the $a(X) \cdot b(X) - c(X) = 0$ relation:
331 $$e([a(\tau)]_1, [b(\tau)]_2) \stackrel{?}{=} e([q(\tau)]_1, [z(\tau)]_2) \cdot e([c(s)]_1, [1]_2)$$
332 which ensures that $\exists~ q(X) \in \mathbb{F}[X] ~\text{s.th.}~ a(X) b(X) - c(X) = q(X) z(X)$.
333\end{enumerate}
334
335
336\vspace{1cm}
337
338\section{Powers of tau (trusted setup)}
339\subsection{Main idea}
340% TODO. mention "SRS" concept
341
342\subsection{Participant contribution}
343In the context of SRS (Structured Reference String), the powers of tau consist of an array containing the scalar multiplication of the generator point by each power of tau, eg. $\tau^0 \cdot G,~\tau^1 \cdot G,~\tau^2 \cdot G,~\tau^3 \cdot G \ldots$
344
345For our case, we'll generate $n$ powers of tau on $\mathbb{G}_1$, and $m$ on $\mathbb{G}_2$. We will denote the combination of both $\mathbb{G}_1$ and $\mathbb{G}_2$ powers of tau by SRS.
346
347Each participant will obtain the previous-participant generated SRS, which is formed by
348
349\begin{align*}
350 \{ [\tau^0]_1, [\tau^1]_1, [\tau^2]_2, \ldots, [\tau^{n-1}]_1 \},\\
351 \{ [\tau^0]_2, [\tau^1]_2, [\tau^2]_2, \ldots, [\tau^{m-1}]_2 \}
352\end{align*}
353
354for simplicity, we will represent it as
355
356$$\{~[~\tau^i]_1~\}^{n-1}_{i=0},~\{~[~\tau^i]_2~\}^{m-1}_{j=0}$$
357
358
359Each participant generates their secret random tau $\tau_p$, which to avoid confusion we will denote as $p \in \mathbb{F}_r$. From it, the participant can compute $[p]_2 \in \mathbb{G}_2$.
360
361Then the participant proceeds to update the reference string (SRS), by multiplying each element by $p^i$:
362$$\{~ p^i \cdot [~ \tau^i]_1~\}^{n-1}_{i=0},~\{~ p^i \cdot [~\tau^i]_2~\}^{m-1}_{j=0}$$
363which, by the properties of scalar multiplication of a point, is equivalent to
364$$\{~ [~ (p \cdot \tau)^i]_1~\}^{n-1}_{i=0},~\{~ [~ (p \cdot \tau)^i]_2~\}^{m-1}_{j=0}$$
365and we denote $p \cdot \tau$ as $\tau'$, so we can write the previous expression as
366$$\{~[~\tau'^i]_1~\}^{n-1}_{i=0},~\{~[~\tau'^i]_2~\}^{m-1}_{j=0}$$
367
368which is
369\begin{align*}
370 \{ [(\tau \cdot p)^0]_1, [(\tau \cdot p)^1]_1, [(\tau \cdot p)^2]_2, \ldots, [(\tau \cdot p)^{n-1}]_1 \},\\
371 \{ [(\tau \cdot p)^0]_2, [(\tau \cdot p)^1]_2, [(\tau \cdot p)^2]_2, \ldots, [(\tau \cdot p)^{m-1}]_2 \}
372\end{align*}
373
374Notice that the contributor does not know the previous $\tau$, but can obtain $(\tau \cdot p)^i$.
375
376
377\subsection{Proof of correct computation}
378The participant will compute the proof, which consists of
379$$\pi = ([\tau']_1,~[p]_2)$$
380which is equivalent to $\pi = (\tau' \cdot G,~p \cdot H) = ((p \cdot \tau) \cdot G,~p \cdot H)$
381
382In the next section we will see how this is used to verify the contribution correct computation.
383
384
385\subsection{Contribution verification}
386This is the interesting part. We want to check that the new SRS is well computed from the previous SRS together with the new tau. We want to avoid accepting contributions that do not follow the powers of tau structure, or that contain empty elements or that do not derive from the previous SRS.
387
388Following the powers of tau structure means that
389$$\tau'^{i+1} = \tau' \cdot \tau'^i ~~\forall~i \in [1, n-1]$$
390
391And the relation between the new SRS and the previous SRS is
392$$\tau' = \tau \cdot p$$
393where $\tau$ is the secret element from the previous SRS and $p$ is the secret one from the new SRS, resulting in the combined $\tau'$.
394
395Now, we're interested into how we can check these relations in the context of the SRS elements. A new contribution can be verified as follows:
396
397\begin{enumerate}
398 \item Check that elements of the new SRS are non-empty, non-zero and in the correct prime order subgroups.
399\item Get the proof ($\pi = ([\tau']_1, [p]_2)$), and confirm that the 1st element is equal to the element in position 1 $[\tau'^1]_1$ of the new SRS (which corresponds to $\tau'$ powered to $1$).
400
401\item Check that $\tau'$ (the new SRS) is correctly related to $\tau$ (the previous SRS).
402
403 To check this, we rely on the pairing properties and we use the proof value generated by the contributor, which consists of $[p]_2$
404 $$e([\tau]_1, [p]_2) \stackrel{?}{=} e([\tau']_1, [1]_2)$$
405
406 We can see how this holds, as $\tau' = p \cdot \tau$, and by the bilinear property of the pairing (see \cite{pairings}) we have $e(a \cdot G, b \cdot H) = e((a \cdot b) \cdot G, H)$, which in our notation is represented as
407 $$e([a]_1, [b]_2) = e([a \cdot b]_1, [1]_2)$$
408 by applying this to our case we can see that:
409 $$e([\tau]_1, [p]_2) = e([\tau \cdot p]_1, [1]_2) = e([\tau']_1, [1]_2)$$
410
411\item Check if the new SRS follows the powers of tau structure:
412 $$e([\tau'^i]_1, [\tau']_2) \stackrel{?}{=} e([\tau'^{i+1}]_1, [1]_2) ~~ \forall ~i \in [1, n-1]$$
413 $$e([\tau']_1, [\tau'^j]_2) \stackrel{?}{=} e([1]_1, [\tau'^{j+1}]_2) ~~ \forall ~i \in [1, m-1]$$
414
415 Which, again, by the bilinarity property, we can see that
416 $$e([\tau'^i]_1, [\tau']_2) = e([\tau'^{i+1}]_1, [1]_2)$$
417 is enforcing that $\tau'^i \cdot \tau'^1 = \tau'^{i+1}$.
418
419 And the same for
420 $$e([\tau']_1, [\tau'^j]_2) = e([1]_1, [\tau'^{j+1}]_2)$$
421 which checks that $\tau'^1 \cdot \tau'^j = \tau'^{j+1}$.
422
423 With this check, we're ensuring that each power of tau of the SRS is consistent with the previous one.
424\end{enumerate}
425
426
427% TODO
428% - uniformize x & X at polynomials notation (currently using p(x) and p(X), uniformize it)
429
430
431\bibliographystyle{unsrt}
432\bibliography{pinocchio-groth16.bib}
433
434\end{document}