feat: make Op Stack Table variable length

This constitutes a major change to the Op Stack Table, including its
AET and AIR. The Processor Table is affected slightly, updating the
Permutation Argument with the Op Stack Table only if the op stack
underflow changes.

specification/src/clock-jump-differences-and-inner-sorting.md

@@ -1,6 +1,6 @@
 # Clock Jump Differences and Inner Sorting
 
-The previous sections show how it is proven that in the JumpStack, OpStack, and RAM Tables, the regions of constant memory pointer are contiguous. The next step is to prove that within each contiguous region of constant memory pointer, the rows are sorted for clock cycle. That is the topic of this section.
+The previous sections show how it is proven that in the Jump Stack, Op Stack, and RAM Tables, the regions of constant memory pointer are contiguous. The next step is to prove that within each contiguous region of constant memory pointer, the rows are sorted for clock cycle. That is the topic of this section.
 
 The problem arises from *clock jumps*, which describes the phenomenon when the clock cycle increases even though the memory pointer does not change.
 If arbitrary jumps were allowed, nothing would prevent the cheating prover from using a table where higher rows correspond to later states, giving rise to an exploitable attack.

specification/src/contiguity-of-memory-pointer-regions.md

@@ -1,15 +1,17 @@
 # Contiguity of Memory-Pointer Regions
 
-## Contiguity for OpStack Table
+## Contiguity for Op Stack Table
 
-In each cycle, the memory pointer for the OpStack Table, `osp`, can only ever increase by one, remain the same, or decrease by one. As a result, it is easy to enforce that the entire table is sorted for memory pointer using one initial constraint and one transition constraint.
+In each cycle, the memory pointer for the Op Stack Table, `op_stack_pointer`, can only ever increase by one, remain the same, or decrease by one.
+As a result, it is easy to enforce that the entire table is sorted for memory pointer using one initial constraint and one transition constraint.
 
- - Initial constraint: `osp` starts with zero, so in terms of polynomials the constraint is `osp`.
- - Transition constraint: the new `osp` is either the same as the previous or one larger. The polynomial representation for this constraint is `(osp' - osp - 1) * (osp' - osp)`.
+ - Initial constraint: `op_stack_pointer` starts with 16[^op_stack], so in terms of polynomials the constraint is `op_stack_pointer - 16`.
+ - Transition constraint: the new `op_stack_pointer` is either the same as the previous or one larger.
+    The polynomial representation for this constraint is `(op_stack_pointer' - op_stack_pointer - 1) · (op_stack_pointer' - op_stack_pointer)`.
 
-## Contiguity for JumpStack Table
+## Contiguity for Jump Stack Table
 
-Analogously to the OpStack Table, the JumpStack's memory pointer `jsp` can only ever decrease by one, remain the same, or increase by one, within each cycle. As a result, similar constraints establish that the entire table is sorted for memory pointer.
+Analogously to the Op Stack Table, the Jump Stack's memory pointer `jsp` can only ever decrease by one, remain the same, or increase by one, within each cycle. As a result, similar constraints establish that the entire table is sorted for memory pointer.
 
  - Initial constraint: `jsp` starts with zero, so in terms of polynomials the constraint is `jsp`.
  - Transition constraint: the new `jsp` is either the same as the previous or one larger. The polynomial representation for this constraint is `(jsp' - jsp - 1) * (jsp' - jsp)`.
@@ -147,3 +149,7 @@ None.
 ### Terminal
 
  - `bc0 ⋅ rpp + bc1 ⋅ fd - 1`
+
+---
+
+[^op_stack]: See [data structures](data-structures.md#operational-stack) and [registers](registers.md#stack) for explanations of the specific value 16.

specification/src/data-structures.md

@@ -1,28 +1,35 @@
 # 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. *OpStack 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
 
 The stack is a last-in;first-out data structure that allows the program to store intermediate variables, pass arguments, and keep pointers to objects held in RAM.
-In this document, the operational stack is either referred to as just “stack” or, if more clarity is desired, “OpStack.”
+In this document, the operational stack is either referred to as just “stack” or, if more clarity is desired, “op stack.”
 
 From the Virtual Machine's point of view, the stack is a single, continuous object.
 The first 16 elements of the stack can be accessed very conveniently.
 Elements deeper in the stack require removing some of the higher elements, possibly after storing them in RAM.
 
 For reasons of arithmetization, the stack is actually split into two distinct parts:
 1. the _operational stack registers_ `st0` through `st15`, and
-1. the _OpStack Underflow Memory_.
+1. the _Op Stack Underflow Memory_.
 
-The motivation and the interplay between the two parts is described and exemplified in [arithmetization of the OpStack table](operational-stack-table.md).
+The motivation and the interplay between the two parts is described and exemplified in [arithmetization of the Op Stack table](operational-stack-table.md).
 
 ## Random Access Memory
 
@@ -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.
 
 ---
 

specification/src/hash-table.md

@@ -1,6 +1,6 @@
 # Hash Table
 
-The instruction `hash` hashes the OpStack's 10 top-most elements in one cycle.
+The instruction `hash` hashes the Op Stack's 10 top-most elements in one cycle.
 Similarly, the Sponge instructions `sponge_init`, `sponge_absorb`, and `sponge_squeeze` also all complete in one cycle.
 The main processor achieves this by using a hash coprocessor.
 The Hash Table is part of the arithmetization of that coprocessor, the other two parts being the [Cascade Table](cascade-table.md) and the [Lookup Table](lookup-table.md).

specification/src/img/aet-relations.ipe

@@ -1,7 +1,7 @@
 <?xml version="1.0"?>
 <!DOCTYPE ipe SYSTEM "ipe.dtd">
 <ipe version="70218" creator="Ipe 7.2.24">
-<info created="D:20200729150742" modified="D:20230627105938"/>
+<info created="D:20200729150742" modified="D:20231024132138"/>
 <preamble>\usepackage{lmodern}
 \renewcommand*\familydefault{\sfdefault}
 \usepackage[T1]{fontenc}</preamble>
@@ -354,7 +354,7 @@ h
 236 128 c
 216 128 l
 </path>
-<path layer="perm_args" stroke="darkblue" pen="heavier" cap="1" join="1" arrow="pointed/small" rarrow="pointed/small">
+<path layer="perm_args" stroke="darkblue" pen="heavier" cap="1" join="1" arrow="pointed/small" rarrow="farc/small">
 180 124 m
 180 108 l
 180 104

specification/src/instruction-groups.md

@@ -197,8 +197,8 @@ Contains all constraints from instruction group `keep_jump_stack`, and additiona
 1. The stack element in `st12` is moved into `st13`.
 1. The stack element in `st13` is moved into `st14`.
 1. The stack element in `st14` is moved into `st15`.
-1. The stack element in `st15` is moved to the top of OpStack underflow, i.e., `osv`.
-1. The OpStack pointer is incremented by 1.
+1. The op stack pointer is incremented by 1.
+1. The running product for the Op Stack Table absorbs the current row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
 
 ### Polynomials
 
@@ -216,8 +216,8 @@ Contains all constraints from instruction group `keep_jump_stack`, and additiona
 1. `st13' - st12`
 1. `st14' - st13`
 1. `st15' - st14`
-1. `osv' - st15`
-1. `osp' - (osp + 1)`
+1. `op_stack_pointer' - (op_stack_pointer + 1)`
+1. `RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊·ib1 - 🍉·op_stack_pointer - 🫒·st15)`
 
 ## Group `grow_stack`
 
@@ -240,8 +240,8 @@ Contains all constraints from instruction group `stack_grows_and_top_2_unconstra
 1. The stack element in `st13` does not change.
 1. The stack element in `st14` does not change.
 1. The stack element in `st15` does not change.
-1. The top of the OpStack underflow, i.e., `osv`, does not change.
-1. The OpStack pointer does not change.
+1. The op stack pointer does not change.
+1. The running product for the Op Stack Table remains unchanged.
 
 ### Polynomials
 
@@ -250,8 +250,8 @@ Contains all constraints from instruction group `stack_grows_and_top_2_unconstra
 1. `st13' - st13`
 1. `st14' - st14`
 1. `st15' - st15`
-1. `osv' - osv`
-1. `osp' - osp`
+1. `op_stack_pointer' - op_stack_pointer`
+1. `RunningProductOpStackTable' - RunningProductOpStackTable`
 
 ## Group `stack_remains_and_top_10_unconstrained`
 
@@ -317,8 +317,8 @@ Contains all constraints from instruction group `unary_operation`, and additiona
 
 ## Group `stack_shrinks_and_top_3_unconstrained`
 
-This instruction group requires helper variable `hv0` to hold the multiplicative inverse of `(osp - 16)`.
-In effect, this means that the OpStack pointer can only be decremented if it is not 16, i.e., if OpStack Underflow Memory is not empty.
+This instruction group requires helper variable `hv0` to hold the multiplicative inverse of `(op_stack_pointer - 16)`.
+In effect, this means that the op stack pointer can only be decremented if it is not 16, i.e., if op stack underflow memory is not empty.
 Since the stack can only change by one element at a time, this prevents stack underflow.
 
 ### Description
@@ -335,9 +335,9 @@ Since the stack can only change by one element at a time, this prevents stack un
 1. The stack element in `st13` is moved into `st12`.
 1. The stack element in `st14` is moved into `st13`.
 1. The stack element in `st15` is moved into `st14`.
-1. The stack element at the top of OpStack underflow, i.e., `osv`, is moved into `st15`.
-1. The OpStack pointer is decremented by 1.
-1. The helper variable register `hv0` holds the inverse of `(osp - 16)`.
+1. The op stack pointer is decremented by 1.
+1. The helper variable register `hv0` holds the inverse of `(op_stack_pointer - 16)`.
+1. The running product for the Op Stack Table absorbs clock cycle and instruction bit 1 from the current row as well as op stack pointer and stack element 15 from the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
 
 ### Polynomials
 
@@ -353,9 +353,9 @@ Since the stack can only change by one element at a time, this prevents stack un
 1. `st12' - st13`
 1. `st13' - st14`
 1. `st14' - st15`
-1. `st15' - osv`
-1. `osp' - (osp - 1)`
-1. `(osp - 16)·hv0 - 1`
+1. `op_stack_pointer' - (op_stack_pointer - 1)`
+1. `(op_stack_pointer - 16)·hv0 - 1`
+1. `RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊·ib1 - 🍉·op_stack_pointer' - 🫒·st15')`
 
 ## Group `binary_operation`
 

specification/src/instruction-specific-transition-constraints.md

@@ -134,8 +134,8 @@ Additionally, it defines the following transition constraints.
 1. If `i` is not 13, then `st13` does not change.
 1. If `i` is not 14, then `st14` does not change.
 1. If `i` is not 15, then `st15` does not change.
-1. The top of the OpStack underflow, i.e., `osv`, does not change.
-1. The OpStack pointer does not change.
+1. The op stack pointer does not change.
+1. The running product for the Op Stack Table remains unchanged.
 
 ### Polynomials
 
@@ -185,8 +185,8 @@ Additionally, it defines the following transition constraints.
 1. `(1 - ind_13(hv3, hv2, hv1, hv0))·(st13' - st13)`
 1. `(1 - ind_14(hv3, hv2, hv1, hv0))·(st14' - st14)`
 1. `(1 - ind_15(hv3, hv2, hv1, hv0))·(st15' - st15)`
-1. `osv' - osv`
-1. `osp' - osp`
+1. `op_stack_pointer' - op_stack_pointer`
+1. `RunningProductOpStackTable' - RunningProductOpStackTable`
 
 ### Helper variable definitions for `swap` + `i`