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

Base Columns

The Operational Stack Table consists of 4 columns:

1. the cycle counter clk
2. the shrink stack indicator shrink_stack
3. the operational stack value osv, and
4. the operational stack pointer osp.

Columns clk, shrink_stack, osp, and osv correspond to columns clk, ib1, osp, and osv in the Processor Table, respectively. A Permutation Argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical.

In order to guarantee memory consistency, the rows of the operational stack table are sorted by operational stack pointer osp 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 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. TritonVM has 16 stack registers, st0 through st15.

Execution trace:

Operational Stack Table:

Extension Columns

The Op Stack Table has 2 extension 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

A padding row is a direct copy of the Op Stack Table's row with the highest value for column clk, called template row, with the exception of the cycle count column clk. In a padding row, the value of column clk is 1 greater than the value of column clk in the template row. The padding row is inserted right below the template row. These steps are repeated until the desired padded height is reached. In total, above steps ensure that the Permutation Argument between the Op Stack Table and the Processor Table holds up.

Memory-Consistency

Memory-consistency follows from two more primitive properties:

1. Contiguity of regions of constant memory pointer. Since the memory pointer for the Op Stack table, osp 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. clk is 0
2. osv is 0.
3. osp is the number of available stack registers, i.e., 16.
4. 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 🪤.
5. The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

1. clk
2. osv
3. osp - 16
4. rppa - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒osv)
5. ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

1. • the osp increases by 1, or
   • the osp does not change AND the osv does not change, or
   • the osp does not change AND the shrink stack indicator shrink_stack is 1.
2. The running product for the permutation argument with the Processor Table rppa absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
3. If the op stack pointer osp 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 same.

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

1. • the osp increases by 1 or the osp does not change
   • the osp increases by 1 or the osv does not change or the shrink stack indicator shrink_stack is 1
2. rppa' = rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')
3. • the osp changes or the logarithmic derivative accumulates a summand, and
   • the osp does not change or the logarithmic derivative does not change.

Transition Constraints as Polynomials

1. (osp' - (osp + 1))·(osp' - osp)
2. (osp' - (osp + 1))·(osv' - osv)·(1 - shrink_stack)
3. rppa' - rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')
4. (osp' - (osp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (osp' - osp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

None.