Skip to content

Commit

Permalink
doc: prose and example for Op Stack Table behavior
Browse files Browse the repository at this point in the history
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed Oct 24, 2023
1 parent eb8dc84 commit db01232
Show file tree
Hide file tree
Showing 5 changed files with 241 additions and 119 deletions.
15 changes: 12 additions & 3 deletions specification/src/data-structures.md
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,20 @@
# Data Structures

## Memory

The term *memory* refers to a data structure that gives read access (and possibly write access, too) to elements indicated by an *address*.
Regardless of the data structure, the address lives in the B-field.
There are four separate notions of memory:

1. *Program Memory*, from which the VM reads instructions.
1. *Op Stack Memory*, which stores the operational stack.
1. *RAM*, to which the VM can read and write field elements.
2. *Program Memory*, from which the VM reads instructions.
3. *Op Stack Memory*, which stores the operational stack.
4. *Jump Stack Memory*, which stores the entire jump stack.
1. *Jump Stack Memory*, which stores the entire jump stack.

## Program Memory

Program memory holds the instructions of the program currently executed by Triton VM.
It is immutable.

## Operational Stack

Expand Down Expand Up @@ -36,8 +43,10 @@ This initialization is one form of secret input, and one of two mechanisms that
The other mechanism is [dedicated instructions](instructions.md#opstack-manipulation).

## Jump Stack

Another last-in;first-out data structure that keeps track of return and destination addresses.
This stack changes only when control follows a `call` or `return` instruction.
Furthermore, executing instruction `recurse` requires a non-empty jump stack.

---

Expand Down
155 changes: 83 additions & 72 deletions specification/src/operational-stack-table.md
View file
Original file line number Diff line number Diff line change
@@ -1,97 +1,104 @@
# Operational Stack Table

The operational stack is where the program stores simple elementary operations, function arguments, and pointers to important objects.
The [operational stack](data-structures.md#operational-stack)[^abbrev] is where the program stores simple elementary operations, function arguments, and pointers to important objects.
There are 16 registers (`st0` through `st15`) that the program can access directly.
These registers correspond to the top of the stack.
They are recorded in the [Processor Table](processor-table.md).

The rest of the operational stack is stored in a dedicated memory object called “operational stack underflow memory”.
The rest of the op stack is stored in a dedicated memory object called “operational stack underflow memory”.
It is initially empty.
The evolution of the underflow memory is recorded in the Operational Stack Table.
The evolution of the underflow memory is recorded in the Op Stack Table.
The sole task of the Op Stack Table is to keep underflow memory immutable.
To achieve this, any read or write accesses to the underflow memory are recorded in the Op Stack Table.
Read and write accesses to op stack underflow memory are a side effect of shrinking or growing the op stack.

## Base Columns

The Operational Stack Table consists of 4 columns:
The Op Stack Table consists of 4 columns:
1. the cycle counter `clk`
1. the shrink stack indicator `shrink_stack`
1. the operational stack value `osv`, and
1. the operational stack pointer `osp`.
1. the shrink stack indicator `shrink_stack`, corresponding to the processor's instruction bit 1 `ib1`,
1. the op stack pointer `stack_pointer`, and
1. the first underflow element `first_underflow_element`.

| Clock | Shrink Stack Indicator | Op Stack Pointer | Op Stack Value |
|:------|:-----------------------|:-----------------|:---------------|
| - | - | - | - |
| Clock | Shrink Stack Indicator | Stack Pointer | First Underflow Element |
|:------|:-----------------------|:--------------|:------------------------|
| - | - | - | - |

Columns `clk`, `shrink_stack`, `osp`, and `osv` correspond to columns `clk`, `ib1`, `osp`, and `osv` in the [Processor Table](processor-table.md), respectively.
A [Permutation Argument](permutation-argument.md) with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical.
Column `clk` records the processor's execution cycle during which the read or write access happens.
The `shrink_stack` indicator signals whether the underflow memory access is a read or a write:
a read corresponds to a shrinking stack is indicated by a 1, a write corresponds to a growing stack and is indicated by a 0.
The same column doubles up as a [padding indicator](#padding), in which case `shrink_stack` is set to 2.
The `stack_pointer` is the address at which the to-be-read-or-written element resides.
Finally, the `first_underflow_element` is the stack element being transferred from stack register `st15` into underflow memory on a write, or the other way around on a read.

In order to guarantee [memory consistency](memory-consistency.md), the rows of the operational stack table are sorted by operational stack pointer `osp` first, cycle count `clk` second.
A [subset Permutation Argument](permutation-argument.md) with the [Processor Table](processor-table.md) establishes that the rows recorded in the Op Stack Table are consistent with the processor's part of the op stack.

In order to guarantee [memory consistency](memory-consistency.md), the rows of the operational stack table are sorted by `stack_pointer` first, cycle count `clk` second.
The mechanics are best illustrated by an example.
Observe how the malicious manipulation of the Op Stack Underflow Memory, the change of “42” into “99” in cycle 8, is detected:
The transition constraints of the Op Stack Table stipulate that if `osp` does not change, then `osv` can only change if the shrink stack indicator `shrink_stack` is set.
Consequently, row `[5, push, 9, 42]` being followed by row `[_, _, 9, 99]` violates the constraints.
The transition constraints of the Op Stack Table stipulate that if `stack_pointer` does not change, then the `first_underflow_element` can only change if the next instruction grows the stack.
Consequently, row `[4, 0, 8, 42]` being followed by row `[10, 1, 8, 99]` violates the constraints.
The shrink stack indicator being correct is guaranteed by the Permutation Argument between Op Stack Table and the [Processor Table](processor-table.md).

For illustrative purposes only, we use four stack registers `st0` through `st3` in the example.
TritonVM has 16 stack registers, `st0` through `st15`.

Execution trace:

| `clk` | `ci` | `nia` | `st0` | `st1` | `st2` | `st3` | Op Stack Underflow Memory | `osp` | `osv` |
|------:|:-------|:-------|------:|------:|------:|------:|:--------------------------|------:|------:|
| 0 | `push` | 42 | 0 | 0 | 0 | 0 | [ ] | 4 | 0 |
| 1 | `push` | 43 | 42 | 0 | 0 | 0 | [0] | 5 | 0 |
| 2 | `push` | 44 | 43 | 42 | 0 | 0 | [0,0] | 6 | 0 |
| 3 | `push` | 45 | 44 | 43 | 42 | 0 | [0,0,0] | 7 | 0 |
| 4 | `push` | 46 | 45 | 44 | 43 | 42 | [0,0,0,0] | 8 | 0 |
| 5 | `push` | 47 | 46 | 45 | 44 | 43 | [42,0,0,0,0] | 9 | 42 |
| 6 | `push` | 48 | 47 | 46 | 45 | 44 | [43,42,0,0,0,0] | 10 | 43 |
| 7 | `nop` | `pop` | 48 | 47 | 46 | 45 | [44,43,42,0,0,0,0] | 11 | 44 |
| 8 | `pop` | `pop` | 48 | 47 | 46 | 45 | [44,43,99,0,0,0,0] | 11 | 44 |
| 9 | `pop` | `pop` | 47 | 46 | 45 | 44 | [43,99,0,0,0,0] | 10 | 43 |
| 10 | `pop` | `pop` | 46 | 45 | 44 | 43 | [99,0,0,0,0] | 9 | 99 |
| 11 | `pop` | `push` | 45 | 44 | 43 | 99 | [0,0,0,0] | 8 | 0 |
| 12 | `push` | 77 | 44 | 43 | 99 | 0 | [0,0,0] | 7 | 0 |
| 13 | `swap` | 4 | 77 | 44 | 43 | 99 | [0,0,0,0] | 8 | 0 |
| 14 | `push` | 78 | 99 | 44 | 43 | 77 | [0,0,0,0] | 8 | 0 |
| 15 | `swap` | 4 | 78 | 99 | 44 | 43 | [77,0,0,0,0] | 9 | 77 |
| 16 | `push` | 79 | 43 | 99 | 44 | 78 | [77,0,0,0,0] | 9 | 77 |
| 17 | `pop` | `pop` | 79 | 43 | 99 | 44 | [78,77,0,0,0,0] | 10 | 78 |
| 18 | `pop` | `pop` | 43 | 99 | 44 | 78 | [77,0,0,0,0] | 9 | 77 |
| 19 | `pop` | `pop` | 99 | 44 | 78 | 77 | [0,0,0,0] | 8 | 0 |
| 20 | `pop` | `pop` | 44 | 78 | 77 | 0 | [0,0,0] | 7 | 0 |
| 21 | `pop` | `pop` | 78 | 77 | 0 | 0 | [0,0] | 6 | 0 |
| 22 | `pop` | `pop` | 77 | 0 | 0 | 0 | [0] | 5 | 0 |
| 23 | `pop` | `pop` | 0 | 0 | 0 | 0 | [ ] | 4 | 0 |
| 24 | `pop` | `nop` | 0 | 0 | 0 | 0 | 💥 | 3 | 0 |
Triton VM has 16 stack registers, `st0` through `st15`.
Furthermore, implied next instructions usually recorded in register “next instruction or argument” `nia` are omitted for reasons of readability.

Processor's execution trace:

| `clk` | `ci` | `nia` | `st0` | `st1` | `st2` | `st3` | Op Stack Underflow Memory | `op_stack_pointer` |
|------:|:-----|------:|------:|------:|------:|------:|:--------------------------|-------------------:|
| 0 | push | 42 | 0 | 0 | 0 | 0 | [] | 4 |
| 1 | push | 43 | 42 | 0 | 0 | 0 | [ 0] | 5 |
| 2 | push | 44 | 43 | 42 | 0 | 0 | [ 0, 0] | 6 |
| 3 | push | 45 | 44 | 43 | 42 | 0 | [ 0, 0, 0] | 7 |
| 4 | push | 46 | 45 | 44 | 43 | 42 | [ 0, 0, 0, 0] | 8 |
| 5 | push | 47 | 46 | 45 | 44 | 43 | [42, 0, 0, 0, 0] | 9 |
| 6 | push | 48 | 47 | 46 | 45 | 44 | [43, 42, 0, 0, 0, 0] | 10 |
| 7 | nop | | 48 | 47 | 46 | 45 | [44, 43, 42, 0, 0, 0] | 11 |
| 8 | pop | | 48 | 47 | 46 | 45 | [44, 43, 99, 0, 0, 0] | 11 |
| 9 | pop | | 47 | 46 | 45 | 44 | [43, 99, 0, 0, 0, 0] | 10 |
| 10 | pop | | 46 | 45 | 44 | 43 | [99, 0, 0, 0, 0] | 9 |
| 11 | pop | | 45 | 44 | 43 | 99 | [ 0, 0, 0, 0] | 8 |
| 12 | push | 77 | 44 | 43 | 99 | 0 | [ 0, 0, 0] | 7 |
| 13 | swap | 3 | 77 | 44 | 43 | 99 | [ 0, 0, 0, 0] | 8 |
| 14 | push | 78 | 99 | 44 | 43 | 77 | [ 0, 0, 0, 0] | 8 |
| 15 | swap | 3 | 78 | 99 | 44 | 43 | [77, 0, 0, 0, 0] | 9 |
| 16 | push | 79 | 43 | 99 | 44 | 78 | [77, 0, 0, 0, 0] | 9 |
| 17 | pop | | 79 | 43 | 99 | 44 | [78, 77, 0, 0, 0, 0] | 10 |
| 18 | pop | | 43 | 99 | 44 | 78 | [77, 0, 0, 0, 0] | 9 |
| 19 | pop | | 99 | 44 | 78 | 77 | [ 0, 0, 0, 0] | 8 |
| 20 | pop | | 44 | 78 | 77 | 0 | [ 0, 0, 0] | 7 |
| 21 | pop | | 78 | 77 | 0 | 0 | [ 0, 0] | 6 |
| 22 | pop | | 77 | 0 | 0 | 0 | [ 0] | 5 |
| 23 | halt | | 0 | 0 | 0 | 0 | [] | 4 |


Operational Stack Table:

| `clk` | `shrink_stack` | (comment) | `osp` | `osv` |
|------:|---------------:|:----------|------:|------:|
| 0 | 0 | (`push`) | 4 | 0 |
| 23 | 1 | (`pop`) | 4 | 0 |
| 1 | 0 | (`push`) | 5 | 0 |
| 22 | 1 | (`pop`) | 5 | 0 |
| 2 | 0 | (`push`) | 6 | 0 |
| 21 | 1 | (`pop`) | 6 | 0 |
| 3 | 0 | (`push`) | 7 | 0 |
| 12 | 0 | (`push`) | 7 | 0 |
| 20 | 1 | (`pop`) | 7 | 0 |
| 4 | 0 | (`push`) | 8 | 0 |
| 11 | 1 | (`pop`) | 8 | 0 |
| 13 | 0 | (`swap`) | 8 | 0 |
| 14 | 0 | (`push`) | 8 | 0 |
| 19 | 1 | (`pop`) | 8 | 0 |
| 5 | 0 | (`push`) | 9 | 42 |
| 10 | 1 | (`pop`) | 9 | 99 |
| 15 | 0 | (`swap`) | 9 | 77 |
| 16 | 0 | (`push`) | 9 | 77 |
| 18 | 1 | (`pop`) | 9 | 77 |
| 6 | 0 | (`push`) | 10 | 43 |
| 9 | 1 | (`pop`) | 10 | 43 |
| 17 | 1 | (`pop`) | 10 | 78 |
| 7 | 0 | (`nop`) | 11 | 44 |
| 8 | 1 | (`pop`) | 11 | 44 |
| `clk` | `shrink_stack` | `stack_pointer` | `first_underflow_element` |
|------:|---------------:|----------------:|--------------------------:|
| 0 | 0 | 4 | 0 |
| 22 | 1 | 4 | 0 |
| 1 | 0 | 5 | 0 |
| 21 | 1 | 5 | 0 |
| 2 | 0 | 6 | 0 |
| 20 | 1 | 6 | 0 |
| 3 | 0 | 7 | 0 |
| 11 | 1 | 7 | 0 |
| 12 | 0 | 7 | 0 |
| 19 | 1 | 7 | 0 |
| 4 | 0 | 8 | 42 |
| 10 | 1 | 8 | 99 |
| 14 | 0 | 8 | 77 |
| 18 | 1 | 8 | 77 |
| 5 | 0 | 9 | 43 |
| 9 | 1 | 9 | 43 |
| 16 | 0 | 9 | 78 |
| 17 | 1 | 9 | 78 |
| 6 | 0 | 10 | 44 |
| 8 | 1 | 10 | 44 |


## Extension Columns

Expand Down Expand Up @@ -177,3 +184,7 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as:
## Terminal Constraints

None.

---

[^abbrev]: frequently abbreviated as “Op Stack”
13 changes: 13 additions & 0 deletions specification/src/processor-table.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,19 @@ The Processor Table has the following extension columns, corresponding to [Evalu
1. `U32LookupClientLogDerivative` for the Lookup Argument with the [U32 Table](u32-table.md).
1. `ClockJumpDifferenceLookupServerLogDerivative` for the Lookup Argument of clock jump differences with the [Op Stack Table](operational-stack-table.md), the [RAM Table](random-access-memory-table.md), and the [Jump Stack Table](jump-stack-table.md).

### Permutation Argument with the Op Stack Table

The [Permutation Arguments](permutation-argument.md) with the [Op Stack Table](operational-stack-table.md) `RunningProductOpStackTable` establishes consistency of the op stack underflow memory.
The number of factors incorporated into the running product at any given cycle depends on the executed instruction in this cycle:
for every element pushed to or popped from the stack, there is one factor.
Namely, if the op stack grows, every element spilling from `st15` into op stack underflow memory will be incorporated as one factor;
and if the op stack shrinks, every element from op stack underflow memory being transferred into `st15` will be one factor.

One key insight for this Permutation Argument is that the processor will always have access to the elements that are to be read from or written to underflow memory:
if the instruction grows the op stack, then the elements in question currently reside in the directly accessible, top part of the stack;
if the instruction shrinks the op stack, then the elements in question will be in the top part of the stack in the next cycle.
In either case, the [Transition Constraint](arithmetization.md#arithmetic-intermediate-representation) for the Permutation Argument can incorporate the explicitly listed elements as well as the corresponding trivial-to-compute `op_stack_pointer`.

## Padding

A padding row is a copy of the Processor Table's last row with the following modifications:
Expand Down
2 changes: 1 addition & 1 deletion triton-vm/src/instruction.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -197,7 +197,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
}
}

const fn name(&self) -> &'static str {
pub(crate) const fn name(&self) -> &'static str {
match self {
Pop => "pop",
Push(_) => "push",
Expand Down
Loading

0 comments on commit db01232

Please sign in to comment.