Skip to content

Commit

Permalink
improve formatting and fix some oversights from previous revisions
Browse files Browse the repository at this point in the history
  • Loading branch information
jan-ferdinand committed Aug 11, 2023
1 parent 2dcdad2 commit 03d03f9
Showing 1 changed file with 62 additions and 60 deletions.
122 changes: 62 additions & 60 deletions tips/tip-0008/tip-0008.md
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
# TIP 0008: Continuations

| TIP | 0008 |
|:---------------|:---------------------------------------------------|
| authors: | Alan Szepieniec |
| title: | Continuations |
| status: | draft |
| created: | 2023-08-10 |
| issue tracker: | <https://github.com/TritonVM/triton-vm/pull/219> |
| TIP | 0008 |
|:---------------|:-------------------------------------------------|
| authors: | Alan Szepieniec |
| title: | Continuations |
| status: | draft |
| created: | 2023-08-10 |
| issue tracker: | <https://github.com/TritonVM/triton-vm/pull/219> |

**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.
Expand All @@ -26,24 +26,26 @@ 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;
- ReceiveAndSend: the segment is sandwiched between two others.

### 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

Expand All @@ -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

Expand Down Expand Up @@ -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

Expand All @@ -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.
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.

0 comments on commit 03d03f9

Please sign in to comment.