Skip to content

Commit

Permalink
feat: Introduce instructions pick and place
Browse files Browse the repository at this point in the history 
These two new instructions simplify manipulation of the operational
stack. Instruction `pick` + `i` moves the indicated stack element to the
top of the stack. Instruction `place` + `i` is its dual, moving the top
of the stack to the indicated position.
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed Sep 13, 2024
1 parent 6271c3d commit b769392
Show file tree
Hide file tree
Showing 12 changed files with 335 additions and 33 deletions.
24 changes: 12 additions & 12 deletions specification/src/arithmetization-overview.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,9 @@
| [CascadeTable](cascade-table.md) | 6 | 2 | 12 |
| [LookupTable](lookup-table.md) | 4 | 2 | 10 |
| [U32Table](u32-table.md) | 10 | 1 | 13 |
| DegreeLowering (-/8/4) | 0/113/226 | 0/14/38 | 0/155/340 |
| DegreeLowering (-/8/4) | 0/118/230 | 0/14/38 | 0/160/344 |
| Randomizers | 0 | 1 | 3 |
| **TOTAL** | **149/262/375** | **50/64/88** | **299/454/639** |
| **TOTAL** | **149/267/379** | **50/64/88** | **299/459/643** |
<!-- auto-gen info stop table_overview -->

## Constraints
Expand All @@ -44,14 +44,14 @@ Before automatic degree lowering:
| [U32Table](u32-table.md) | 1 | 15 | 22 | 2 | 12 |
| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | 1 |
| **TOTAL** | **79** | **76** | **150** | **23** | **19** |
| (# nodes) | (534) | (624) | (6176) | (213) | |
| (# nodes) | (534) | (624) | (6679) | (213) | |

After lowering degree to 8:

| table name | #initial | #consistency | #transition | #terminal |
|:-----------------------------------------------|---------:|-------------:|------------:|----------:|
| [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 |
| [ProcessorTable](processor-table.md) | 29 | 10 | 160 | 1 |
| [ProcessorTable](processor-table.md) | 29 | 10 | 165 | 1 |
| [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 |
| [RamTable](random-access-memory-table.md) | 7 | 0 | 12 | 1 |
| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 |
Expand All @@ -60,15 +60,15 @@ After lowering degree to 8:
| [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 |
| [U32Table](u32-table.md) | 1 | 18 | 24 | 2 |
| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 |
| **TOTAL** | **79** | **80** | **273** | **23** |
| (# nodes) | (534) | (635) | (6438) | (213) |
| **TOTAL** | **79** | **80** | **278** | **23** |
| (# nodes) | (534) | (635) | (6956) | (213) |

After lowering degree to 4:

| table name | #initial | #consistency | #transition | #terminal |
|:-----------------------------------------------|---------:|-------------:|------------:|----------:|
| [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 |
| [ProcessorTable](processor-table.md) | 31 | 10 | 234 | 1 |
| [ProcessorTable](processor-table.md) | 31 | 10 | 238 | 1 |
| [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 |
| [RamTable](random-access-memory-table.md) | 7 | 0 | 13 | 1 |
| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 7 | 0 |
Expand All @@ -77,8 +77,8 @@ After lowering degree to 4:
| [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 |
| [U32Table](u32-table.md) | 1 | 26 | 34 | 2 |
| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 |
| **TOTAL** | **81** | **94** | **394** | **23** |
| (# nodes) | (538) | (676) | (6731) | (213) |
| **TOTAL** | **81** | **94** | **398** | **23** |
| (# nodes) | (538) | (676) | (7246) | (213) |
<!-- auto-gen info stop constraints_overview -->


Expand All @@ -90,8 +90,8 @@ In order to gauge the runtime cost for this step, the following table provides e
<!-- auto-gen info start tasm_air_evaluation_cost -->
| Type | Processor | Op Stack | RAM |
|:-------------|----------:|---------:|------:|
| static | 35381 | 65645 | 23226 |
| dynamic | 46805 | 73265 | 27034 |
| static | 37759 | 70227 | 24996 |
| dynamic | 49456 | 78029 | 28895 |
<!-- auto-gen info stop tasm_air_evaluation_cost -->

## Opcode Pressure
Expand All @@ -104,7 +104,7 @@ The table below helps answer this question at a glance.
| IsU32 | ShrinksStack | HasArg | Num Opcodes |
|-------------:|-------------:|-------------:|-------------:|
| n | n | n | 12 |
| n | n | y | 8 |
| n | n | y | 10 |
| n | y | n | 11 |
| n | y | y | 3 |
| y | n | n | 6 |
Expand Down
2 changes: 2 additions & 0 deletions specification/src/instruction-groups.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ A summary of all instructions and which groups they are part of is given in the
| `pop` + `n` | x | x | x | x | | | x | | | | | | | | x |
| `push` + `a` | | | x | x | | | x | x | | | | | | | |
| `divine` + `n` | x | x | x | x | | | x | | x | | | | | | |
| `pick` + `i` | x | | x | x | | | x | | | x | | | | | |
| `place` + `i` | x | | x | x | | | x | | | x | | | | | |
| `dup` + `i` | x | | x | x | | | x | x | | | | | | | |
| `swap` + `i` | x | | x | x | | | x | | | x | | | | | |
| `nop` | | | x | x | | x | | | | x | 0 | x | | | |
Expand Down
24 changes: 24 additions & 0 deletions specification/src/instruction-specific-transition-constraints.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,30 @@ In addition to its [instruction groups](instruction-groups.md), this instruction

This instruction is fully constrained by its [instruction groups](instruction-groups.md)

## Instruction `pick` + `i`

This instruction makes use of [indicator polynomials](instruction-groups.md#indicator-polynomials-ind_ihv3-hv2-hv1-hv0).
In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.

### Description

For 0 ⩽ `i` < 16:
1. Stack element `i` is moved to the top.
1. For 0 ⩽ `j` < `i`: stack element `j` is shifted down by 1.
1. For `j` > `i`: stack element `j` remains unchanged.

## Instruction `place` + `i`

This instruction makes use of [indicator polynomials](instruction-groups.md#indicator-polynomials-ind_ihv3-hv2-hv1-hv0).
In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints.

### Description

For 0 ⩽ `i` < 16:
1. Stack element 0 is moved to position `i`.
1. For 0 ⩽ `j` < `i`: stack element `j` is shifted up by 1.
1. For `j` > `i`: stack element `j` remains unchanged.

## Instruction `dup` + `i`

This instruction makes use of [indicator polynomials](instruction-groups.md#indicator-polynomials-ind_ihv3-hv2-hv1-hv0).
Expand Down
14 changes: 8 additions & 6 deletions specification/src/instructions.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,10 @@ The third property allows efficient arithmetization of the running product for t
| `pop` + `n` | 3 | e.g., `_ c b a` | e.g., `_` | Pops the `n` top elements from the stack. 1 ⩽ `n` ⩽ 5 |
| `push` + `a` | 1 | `_` | `_ a` | Pushes `a` onto the stack. |
| `divine` + `n` | 9 | e.g., `_` | e.g., `_ b a` | Pushes `n` non-deterministic elements `a` to the stack. Interface for secret input. 1 ⩽ `n` ⩽ 5 |
| `dup` + `i` | 17 | e.g., `_ e d c b a` | e.g., `_ e d c b a d` | Duplicates the element `i` positions away from the top. 0 ⩽ `i` < 16 |
| `swap` + `i` | 25 | e.g., `_ e d c b a` | e.g., `_ e a c b d` | Swaps the `i`th stack element with the top of the stack. 0 ⩽ `i` < 16 |
| `pick` + `i` | 17 | e.g., `_ d x c b a` | e.g., `_ d c b a x` | Moves the element indicated by `i` to the top of the stack. 0 ⩽ `i` < 16 |
| `place` + `i` | 25 | e.g., `_ d c b a x` | e.g., `_ d x c b a` | Moves the top of the stack to the indicated position `i`. 0 ⩽ `i` < 16 |
| `dup` + `i` | 33 | e.g., `_ e d c b a` | e.g., `_ e d c b a d` | Duplicates the element `i` positions away from the top. 0 ⩽ `i` < 16 |
| `swap` + `i` | 41 | e.g., `_ e d c b a` | e.g., `_ e a c b d` | Swaps the `i`th stack element with the top of the stack. 0 ⩽ `i` < 16 |

Instruction `divine n` (together with [`merkle_step`](#many-in-one)) make Triton a virtual machine that can execute non-deterministic programs.
As programs go, this concept is somewhat unusual and benefits from additional explanation.
Expand All @@ -46,7 +48,7 @@ the divined values were supplied as and are read from secret input.
| `halt` | 0 | `_` | `_` | `ip` | `ip+1` | `_` | `_` | Solves the halting problem (if the instruction is reached). Indicates graceful shutdown of the VM. |
| `nop` | 8 | `_` | `_` | `ip` | `ip+1` | `_` | `_` | Do nothing |
| `skiz` | 2 | `_ a` | `_` | `ip` | `ip+s` | `_` | `_` | Skip next instruction if `a` is zero. `s` ∈ {1, 2, 3} depends on `a` and whether the next instruction takes an argument. |
| `call` + `d` | 33 | `_` | `_` | `ip` | `d` | `_` | `_ (ip+2, d)` | Push `(ip+2,d)` to the jump stack, and jump to absolute address `d` |
| `call` + `d` | 49 | `_` | `_` | `ip` | `d` | `_` | `_ (ip+2, d)` | Push `(ip+2,d)` to the jump stack, and jump to absolute address `d` |
| `return` | 16 | `_` | `_` | `ip` | `o` | `_ (o, d)` | `_` | Pop one pair off the jump stack and jump to that pair's return address (which is the first element). |
| `recurse` | 24 | `_` | `_` | `ip` | `d` | `_ (o, d)` | `_ (o, d)` | Peek at the top pair of the jump stack and jump to that pair's destination address (which is the second element). |
| `recurse_or_return` | 32 | `_ b a .....` | `_ b a .....` | `ip` | `d` or `o` | `_ (o, d)` | `_ (o, d)` or `_` | Like `recurse` if `st5 = a != b = st6`, like `return` if `a == b`. See also extended description below. |
Expand All @@ -64,7 +66,7 @@ The instruction is designed to facilitate loops using pointer equality as termin

| Instruction | Opcode | old op stack | new op stack | old RAM | new RAM | Description |
|:------------------|-------:|:---------------------|:-----------------------|:--------------------|:--------------------|:---------------------------------------------------------------------------------------------------------------------------------------------|
| `read_mem` + `n` | 41 | e.g., `_ p+2` | e.g., `_ v2 v1 v0 p-1` | [p: v0, p+1, v1, …] | [p: v0, p+1, v1, …] | Reads consecutive values `vi` from RAM at address `p` and puts them onto the op stack. Decrements RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5 |
| `read_mem` + `n` | 57 | e.g., `_ p+2` | e.g., `_ v2 v1 v0 p-1` | [p: v0, p+1, v1, …] | [p: v0, p+1, v1, …] | Reads consecutive values `vi` from RAM at address `p` and puts them onto the op stack. Decrements RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5 |
| `write_mem` + `n` | 11 | e.g., `_ v2 v1 v0 p` | e.g., `_ p+3` | [] | [p: v0, p+1, v1, …] | Writes op stack's `n` top-most values `vi` to RAM at the address `p+i`, popping the `vi`. Increments RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5 |

For the benefit of clarity, the effect of every possible argument is given below.
Expand Down Expand Up @@ -112,7 +114,7 @@ Triton VM cannot know the number of elements that will be absorbed.
| Instruction | Opcode | old op stack | new op stack | Description |
|:-------------|-------:|:-------------|:-------------|:---------------------------------------------------------------------------------------------------------------------------|
| `add` | 42 | `_ b a` | `_ c` | Computes the sum (`c`) of the top two elements of the stack (`b` and `a`) over the field. |
| `addi` + `a` | 49 | `_ b` | `_ c` | Computes the sum (`c`) of the top element of the stack (`b`) and the immediate argument (`a`). |
| `addi` + `a` | 65 | `_ b` | `_ c` | Computes the sum (`c`) of the top element of the stack (`b`) and the immediate argument (`a`). |
| `mul` | 50 | `_ b a` | `_ c` | Computes the product (`c`) of the top two elements of the stack (`b` and `a`) over the field. |
| `invert` | 64 | `_ a` | `_ b` | Computes the multiplicative inverse (over the field) of the top of the stack. Crashes the VM if the top of the stack is 0. |
| `eq` | 58 | `_ b a` | `_ (a == b)` | Tests the top two stack elements for equality. |
Expand Down Expand Up @@ -143,7 +145,7 @@ Triton VM cannot know the number of elements that will be absorbed.

| Instruction | Opcode | old op stack | new op stack | Description |
|:-----------------|-------:|:----------------|:----------------|:-----------------------------------------------------------------------------------------|
| `read_io` + `n` | 49 | e.g., `_` | e.g., `_ c b a` | Reads `n` B-Field elements from standard input and pushes them to the stack. 1 ⩽ `n` ⩽ 5 |
| `read_io` + `n` | 73 | e.g., `_` | e.g., `_ c b a` | Reads `n` B-Field elements from standard input and pushes them to the stack. 1 ⩽ `n` ⩽ 5 |
| `write_io` + `n` | 19 | e.g., `_ c b a` | e.g., `_` | Pops `n` elements from the stack and writes them to standard output. 1 ⩽ `n` ⩽ 5 |

## Many-In-One
Expand Down
Loading

0 comments on commit b769392

Please sign in to comment.