Operational Stack Table

The operational stack¹ 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.

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

Main Columns

The Op Stack Table consists of 4 columns:

1. the cycle counter clk
2. the shrink stack indicator shrink_stack, corresponding to the processor's instruction bit 1 ib1,
3. the op stack pointer stack_pointer, and
4. the first underflow element first_underflow_element.

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, 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.

A subset Permutation Argument with the Processor Table 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, 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 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.

For illustrative purposes only, we use four stack registers st0 through st3 in the example. 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:

Operational Stack Table:

Auxiliary Columns

The Op Stack Table has 2 auxiliary columns, rppa and ClockJumpDifferenceLookupClientLogDerivative.

1. A Permutation Argument establishes that the rows of the Op Stack Table correspond to the rows of the Processor Table. The running product for this argument is contained in the rppa column.
2. In order to achieve memory consistency, a Lookup Argument shows that all clock jump differences are contained in the clk column of the Processor Table. The logarithmic derivative for this argument is contained in the ClockJumpDifferenceLookupClientLogDerivative column.

Padding

The last row in the Op Stack Table is taken as the padding template row. Should the Op Stack Table be empty, the row (clk, shrink_stack, stack_pointer, first_underflow_element) = (0, 0, 16, 0) is used instead. In the template row, the shrink_stack indicator is set to 2, signifying padding. The template row is inserted below the last row until the desired padded height is reached.

Memory-Consistency

Memory-consistency follows from two more primitive properties:

1. Contiguity of regions of constant memory pointer. Since in Op Stack Table, the stack_pointer can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints.
2. Correct inner-sorting within contiguous regions. Specifically, the rows within each contiguous region of constant memory pointer should be sorted for clock cycle. This property is established by the clock jump difference Lookup Argument. In a nutshell, every difference of consecutive clock cycles that occurs within one contiguous block of constant memory pointer is shown itself to be a valid clock cycle through a separate cross-table argument.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Initial Constraints

1. The stack_pointer is the number of available stack registers, i.e., 16.
2. If the row is not a padding row, the running product for the permutation argument with the Processor Table rppa starts off having accumulated the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. Otherwise, it is the Permutation Argument's default initial, i.e., 1.
3. The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

1. stack_pointer - 16
2. (shrink_stack - 2)·(rppa - (🪤 - 🍋·clk - 🍊·shrink_stack - 🍉·stack_pointer - 🫒·first_underflow_element))
+ (shrink_stack - 0)·(shrink_stack - 1)·(rppa - 1)
3. ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

1. • the stack_pointer increases by 1, or
   • the stack_pointer does not change AND the first_underflow_element does not change, or
   • the stack_pointer does not change AND the shrink stack indicator shrink_stack in the next row is 0.
2. If thex next row is not a padding row, the running product for the permutation argument with the Processor Table rppa absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. Otherwise, the running product remains unchanged.
3. If the current row is a padding row, then the next row is a padding row.
4. If the next row is not a padding row and the op stack pointer stack_pointer does not change, then the logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative accumulates a factor (clk' - clk) relative to indeterminate 🪞. Otherwise, it remains the unchanged.

Written as Disjunctive Normal Form, the same constraints can be expressed as:

1. The stack_pointer increases by 1 or the stack_pointer does not change.
2. The stack_pointer increases by 1 or the first_underflow_element does not change or the shrink stack indicator shrink_stack in the next row is 0.
3. • The next row is a padding row or rppa has accumulated the next row, and
   • the next row is not a padding row or rppa remains unchanged.
4. The current row is not a padding row or the next row is a padding row.
5. • the stack_pointer changes or the next row is a padding row or the logarithmic derivative accumulates a summand,
   • the stack_pointer remains unchanged or the logarithmic derivative remains unchanged, and
   • the next row is not a padding row or the logarithmic derivative remains unchanged.

Transition Constraints as Polynomials

1. (stack_pointer' - stack_pointer - 1)·(stack_pointer' - stack_pointer)
2. (stack_pointer' - stack_pointer - 1)·(first_underflow_element' - first_underflow_element)·(shrink_stack' - 0)
3. (shrink_stack' - 2)·(rppa' - rppa·(🪤 - 🍋·clk' - 🍊·shrink_stack' - 🍉·stack_pointer' - 🫒first_underflow_element'))
+ (shrink_stack' - 0)·(shrink_stack' - 1)·(rppa' - rppa)
4. (shrink_stack - 0)·(shrink_stack - 1)·(shrink_stack' - 2)
5. (stack_pointer' - stack_pointer - 1)·(shrink_stack' - 2)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (stack_pointer' - stack_pointer)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)
+ (shrink_stack' - 0)·(shrink_stack' - 1)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

None.