From 03d03f9a281d75ae2059a151c20655d5c8e29d61 Mon Sep 17 00:00:00 2001 From: Jan Ferdinand Sauer Date: Fri, 11 Aug 2023 16:49:29 +0200 Subject: [PATCH] improve formatting and fix some oversights from previous revisions --- tips/tip-0008/tip-0008.md | 122 +++++++++++++++++++------------------- 1 file changed, 62 insertions(+), 60 deletions(-) diff --git a/tips/tip-0008/tip-0008.md b/tips/tip-0008/tip-0008.md index b0ad71402..0a504e1a1 100644 --- a/tips/tip-0008/tip-0008.md +++ b/tips/tip-0008/tip-0008.md @@ -1,12 +1,12 @@ # TIP 0008: Continuations -| TIP | 0008 | -|:---------------|:---------------------------------------------------| -| authors: | Alan Szepieniec | -| title: | Continuations | -| status: | draft | -| created: | 2023-08-10 | -| issue tracker: | | +| TIP | 0008 | +|:---------------|:-------------------------------------------------| +| authors: | Alan Szepieniec | +| title: | Continuations | +| status: | draft | +| created: | 2023-08-10 | +| issue tracker: | | **Abstract.** This note describes an architectural change to Triton VM that enables splitting the algebraic execution trace into separately provable segments and linking the resulting proofs while authenticating the transmitted state. As a result, you can parallelize the generation of proofs for long-running computations. @@ -26,6 +26,7 @@ At the heart of this technique lies the representation of memory as a pair of po ### Proof Types Depending on the nature of the segment in question, the proof type is one of: + - Standalone: no segmentation at all; - ReceiveState: the segment is followed by another but has no predecessor; - SendState: the segment follows after another but is the last one in a sequence; @@ -33,17 +34,18 @@ Depending on the nature of the segment in question, the proof type is one of: ### The State -The state of the VM is fully determined by a bunch of things divisible into three categories: +The state of the VM is fully determined by a bunch of things, divisible into the following categories: - - (a) the program, - - (b) the instruction pointer, which lives in a register, - - (b) the top 16 elements of the operational stack, which live in registers, - - (b) the 16 sponge state elements - - (c) the number of elements that have been read from standard input, (the input itself is part of the claim) - - (c) the number of elements that have been written to standard output, (the output itself is part of the claim) - - (d) the other elements of the operational stack which are stored in OpStack memory, - - (d) the entire JumpStack memory, - - (d) the entire RAM. + (a) the program, + (a) certain registers, namely + + the instruction pointer + + the top 16 elements of the operational stack + + the 16 sponge state elements + (a) the number of read input and output elements, respectively, (input and output themselves are part of the claim), + (a) memory objects, namely + + the other elements of the operational stack which are stored in OpStack memory, + + the entire JumpStack memory, + + the entire RAM. ### (a) Program @@ -59,52 +61,52 @@ To prove the integrity of the state-carrying registers across segments, we conve To convert the state-carrying registers to memory, we assign addresses to them: -| register | address | -|----------|---------| -| `st0` | 0 | -| `st1` | 1 | -| `st2` | 2 | -| `st3` | 3 | -| `st4` | 4 | -| `st5` | 5 | -| `st6` | 6 | -| `st7` | 7 | -| `st8` | 8 | -| `st9` | 9 | -| `st10` | 10 | -| `st11` | 11 | -| `st12` | 12 | -| `st13` | 13 | -| `st14` | 14 | -| `st15` | 15 | -| `sponge0` | 16 | -| `sponge1` | 17 | -| `sponge2` | 18 | -| `sponge3` | 19 | -| `sponge4` | 20 | -| `sponge5` | 21 | -| `sponge6` | 22 | -| `sponge7` | 23 | -| `sponge8` | 24 | -| `sponge9` | 25 | -| `sponge10` | 26 | -| `sponge11` | 27 | -| `sponge12` | 28 | -| `sponge13` | 29 | -| `sponge14` | 30 | -| `sponge15` | 31 | -| `ip` | 32 | +| register | address | +|:-----------|--------:| +| `st0` | 0 | +| `st1` | 1 | +| `st2` | 2 | +| `st3` | 3 | +| `st4` | 4 | +| `st5` | 5 | +| `st6` | 6 | +| `st7` | 7 | +| `st8` | 8 | +| `st9` | 9 | +| `st10` | 10 | +| `st11` | 11 | +| `st12` | 12 | +| `st13` | 13 | +| `st14` | 14 | +| `st15` | 15 | +| `sponge0` | 16 | +| `sponge1` | 17 | +| `sponge2` | 18 | +| `sponge3` | 19 | +| `sponge4` | 20 | +| `sponge5` | 21 | +| `sponge6` | 22 | +| `sponge7` | 23 | +| `sponge8` | 24 | +| `sponge9` | 25 | +| `sponge10` | 26 | +| `sponge11` | 27 | +| `sponge12` | 28 | +| `sponge13` | 29 | +| `sponge14` | 30 | +| `sponge15` | 31 | +| `ip` | 32 | Naturally, the value of the memory object at those addresses corresponds to the value of the matching register. -**Constraints.** Let $Z_{\{0,\ldots,16\}}(X)$ be the zerofier for $\{0, \ldots, 16\}$ and $I_V(X)$ be the interpolant that takes the values of the listed registers on their respective domain points. We need to show that both: +**Constraints.** Let $Z_{\{0,\ldots,32\}}(X)$ be the zerofier for $\{0,\ldots,32\}$ and $I_V(X)$ be the interpolant that takes the values of the listed registers on their respective domain points. We need to show that both: - - $Z_{\{0,\ldots,16\}}(X)$ divides $K(X)$, and - - $Z_{\{0,\ldots,16\}}(X)$ divides $V(X) - I_V(X)$. + - $Z_{\{0,\ldots,32\}}(X)$ divides $K(X)$, and + - $Z_{\{0,\ldots,32\}}(X)$ divides $V(X) - I_V(X)$. -To do this, we commit to $K'(X) = \frac{K(X)}{Z_{\{0,\ldots,16\}}(X)}$ and $V'(X) = \frac{V(X)-I_V(X)}{Z_{\{0,\ldots,16\}}(X)}$ by listing their coefficients in new dedicated columns in the base table. New columns in the extension table prove the correct evaluation of these polynomial. +To do this, we commit to $K'(X) = \frac{K(X)}{Z_{\{0,\ldots,32\}}(X)}$ and $V'(X) = \frac{V(X)-I_V(X)}{Z_{\{0,\ldots,32\}}(X)}$ by listing their coefficients in new dedicated columns in the base table. New columns in the extension table prove the correct evaluation of these polynomial. -Note that we do not even need to commit to $K(X)$ and $V(X)$ directly; we simulate their evaluation in $\alpha$ via $K(\alpha) = K'(\alpha) \cdot Z_{\{0,\ldots,16\}}(\alpha)$ and $V(\alpha) = V'(\alpha) \cdot Z_{\{0,\ldots,16\}}(X) + V_I(\alpha)$. +Note that we do not even need to commit to $K(X)$ and $V(X)$ directly; we simulate their evaluation in $\alpha$ via $K(\alpha) = K'(\alpha) \cdot Z_{\{0,\ldots,32\}}(\alpha)$ and $V(\alpha) = V'(\alpha) \cdot Z_{\{0,\ldots,32\}}(X) + V_I(\alpha)$. ### (c) Input and Output @@ -214,9 +216,9 @@ In regards to the trackers, it is ill-advised to combine them because they may r ## Large Memory -The technique described here is ill-suited when a large number of memory cells are touched. The reason is that the degrees of the memory polynomials is essentially equal to the number of addresses. It's not uncommong for computations to touch gigabytes of memory, but even assuming for simplicity (and contrary to fact) that we can store 8 bytes in a field element, a memory polynomial storing 1 GiB of data would have degree roughly $2^{27}$. +The technique described here is ill-suited when a large number of memory cells are touched. The reason is that the degrees of the memory polynomials is essentially equal to the number of addresses. It's not uncommon for computations to touch gigabytes of memory, but even assuming for simplicity (and contrary to fact) that we can store 8 bytes in a field element, a memory polynomial storing 1 GiB of data would have degree roughly $2^{27}$. -There are two strategies for accomodating continuations for computations that touch a lot of memory explained below. Neither one requires a modification to the architecture of Triton VM as they rely only on clever programming. +There are two strategies for accommodating continuations for computations that touch a lot of memory explained below. Neither one requires a modification to the architecture of Triton VM as they rely only on clever programming. ### Merkleization @@ -228,4 +230,4 @@ To page in, guess the page nondeterministically and hash it to compute the leaf. ### Disk Reads -Use standard input and standard output communicate with the operating system, which performs disk reads and writes on the program's behalf. A separate proof system needs to establish that the list of disk reads and writes is authentic, but the point is that this argument is external to Triton VM and thus out of scope here. \ No newline at end of file +Use standard input and standard output communicate with the operating system, which performs disk reads and writes on the program's behalf. A separate proof system needs to establish that the list of disk reads and writes is authentic, but the point is that this argument is external to Triton VM and thus out of scope here.