Jump Stack Table

The Jump Stack Memory contains the underflow from the Jump Stack.

Main Columns

The Jump Stack Table consists of 5 columns:

1. the cycle counter clk
2. current instruction ci,
3. the jump stack pointer jsp,
4. the last jump's origin jso, and
5. the last jump's destination jsd.

The rows are sorted by jump stack pointer jsp, then by cycle counter clk. The column jsd contains the destination of stack-extending jump (call) as well as of the no-stack-change jump (recurse); the column jso contains the source of the stack-extending jump (call) or equivalently the destination of the stack-shrinking jump (return).

The AIR for this table guarantees that the return address of a single cell of return address memory can change only if there was a call instruction.

An example program, execution trace, and jump stack table are shown below.

Program:

Execution trace:

Jump Stack Table:

Auxiliary Columns

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

1. A Permutation Argument establishes that the rows of the Jump Stack Table match with the rows in 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 Jump 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 Jump 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 Jump Stack table, jsp 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. Cycle count clk is 0.
2. Jump Stack Pointer jsp is 0.
3. Jump Stack Origin jso is 0.
4. Jump Stack Destination jsd is 0.
5. The running product for the permutation argument with the Processor Table rppa has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
6. The running product of clock jump differences ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

1. clk
2. jsp
3. jso
4. jsd
5. rppa - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)
6. ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

1. The jump stack pointer jsp increases by 1, or
2. (jsp does not change and jso does not change and jsd does not change and the cycle counter clk increases by 1), or
3. (jsp does not change and jso does not change and jsd does not change and the current instruction ci is call), or
4. (jsp does not change and the current instruction ci is return), or
5. (jsp does not change and the current instruction ci is recurse_or_return).
6. The running product for the permutation argument rppa absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
7. If the jump stack pointer jsp 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 jump stack pointer jsp increases by 1 or the jump stack pointer jsp does not change
2. The jump stack pointer jsp increases by 1 or the jump stack origin jso does not change or current instruction ci is return or recurse_or_return
3. The jump stack pointer jsp increases by 1 or the jump stack destination jsd does not change or current instruction ci is return or recurse_or_return
4. The jump stack pointer jsp increases by 1 or the cycle count clk increases by 1 or current instruction ci is call or current instruction ci is return or recurse_or_return
5. rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')
6. • the jsp changes or the logarithmic derivative accumulates a summand, and
   • the jsp does not change or the logarithmic derivative does not change.

Transition Constraints as Polynomials

1. (jsp' - (jsp + 1))·(jsp' - jsp)
2. (jsp' - (jsp + 1))·(jso' - jso)·(ci - op_code(return))
3. (jsp' - (jsp + 1))·(jsd' - jsd)·(ci - op_code(return))
4. (jsp' - (jsp + 1))·(clk' - (clk + 1))·(ci - op_code(call))·(ci - op_code(return))
5. clk_di·(jsp' - jsp - 1)·(1 - clk_di·(clk' - clk - one))
6. (clk' - clk - one)·(jsp' - jsp - 1)·(1 - clk_di·(clk' - clk - one))
7. rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')
8. (jsp' - (jsp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (jsp' - jsp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

None.