doc: update Processor Table's AET and AIR

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 op stack underflow, i.e., `osv`.
 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 op stack underflow, i.e., `osv`, 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,7 +317,7 @@ 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)`.
+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.
 
@@ -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 op stack underflow, i.e., `osv`, is moved into `st15`.
 1. The op stack pointer is decremented by 1.
-1. The helper variable register `hv0` holds the inverse of `(osp - 16)`.
+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 op stack underflow, i.e., `osv`, 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`
 

specification/src/processor-table.md

@@ -99,13 +99,12 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th
 1. The operational stack element `st10` is 0.
 1. The [Evaluation Argument](evaluation-argument.md) of operational stack elements `st11` through `st15` with respect to indeterminate 🥬 equals the public part of program digest challenge, 🫑.
 See [program attestation](program-attestation.md) for more details.
-1. The operational stack pointer `osp` is 16.
-1. The operational stack value `osv` is 0.
+1. The `op_stack_pointer` is 16.
 1. The RAM pointer `ramp` is 0.
 1. `RunningEvaluationStandardInput` is 1.
 1. `RunningEvaluationStandardOutput` is 1.
 1. `InstructionLookupClientLogDerivative` has absorbed the first row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥.
-1. `RunningProductOpStackTable` has absorbed the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
+1. `RunningProductOpStackTable` is 1.
 1. `RunningProductRamTable` has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
 1. `RunningProductJumpStackTable` has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
 1. `RunningEvaluationHashInput` has absorbed the first row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪 if the current instruction is `hash`. Otherwise, it is 1.
@@ -134,13 +133,12 @@ See [program attestation](program-attestation.md) for more details.
 1. `st9`
 1. `st10`
 1. `🥬^5 + st11·🥬^4 + st12·🥬^3 + st13·🥬^2 + st14·🥬 + st15 - 🫑`
-1. `osp`
-1. `osv`
+1. `op_stack_pointer - 16`
 1. `ramp`
 1. `RunningEvaluationStandardInput - 1`
 1. `RunningEvaluationStandardOutput - 1`
 1. `InstructionLookupClientLogDerivative · (🪥 - 🥝·ip - 🥥·ci - 🫐·nia) - 1`
-1. `RunningProductOpStackTable - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒·osv)`
+1. `RunningProductOpStackTable - 1`
 1. `RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction)`
 1. `RunningProductJumpStackTable - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)`
 1. `(ci - opcode(hash))·(RunningEvaluationHashInput - 1)`<br />
@@ -189,7 +187,6 @@ The following additional constraints also apply to every pair of rows.
 1. The running evaluation for standard input absorbs `st0` of the next row with respect to 🛏 if the current instruction is `read_io`, and remains unchanged otherwise.
 1. The running evaluation for standard output absorbs `st0` of the next row with respect to 🧯 if the current instruction in the next row is `write_io`, and remains unchanged otherwise.
 1. If the next row is not a padding row, the logarithmic derivative for the Program Table absorbs the next row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥. Otherwise, it remains unchanged.
-1. The running product for the Op Stack Table absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
 1. The running product for the RAM Table absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
 1. The running product for the Jump Stack Table absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
 1. If the current instruction in the next row is `hash`, the running evaluation “Hash Input” absorbs the next row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪. Otherwise, it remains unchanged.
@@ -218,7 +215,6 @@ Otherwise, the running evaluation remains unchanged.
     `+ write_io_deselector'·(RunningEvaluationStandardOutput' - 🧯·RunningEvaluationStandardOutput - st0')`
 1. `(1 - IsPadding') · ((InstructionLookupClientLogDerivative' - InstructionLookupClientLogDerivative) · (🛁 - 🥝·ip' - 🥥·ci' - 🫐·nia') - 1)`<br />
     `+ IsPadding'·(RunningProductInstructionTable' - RunningProductInstructionTable)`
-1. `RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒·osv')`
 1. `RunningProductRamTable' - RunningProductRamTable·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')`
 1. `RunningProductJumpStackTable' - RunningProductJumpStackTable·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')`
 1. `(ci' - opcode(hash))·(RunningEvaluationHashInput' - RunningEvaluationHashInput)`<br />

specification/src/registers.md

@@ -18,7 +18,6 @@ the remaining registers exist only to enable an efficient arithmetization and ar
 | `jsd`                  | jump stack destination                    | contains the argument of the last `call`                                                                                                                                                                                  |
 | `st0` through `st15`   | operational stack registers               | contain explicit operational stack values                                                                                                                                                                                 |
 | *`op_stack_pointer`    | operational stack pointer                 | the current size of the operational stack                                                                                                                                                                                 |
-| *`osv`                 | operational stack value                   | contains the (stack) memory value at the given address                                                                                                                                                                    |
 | *`hv0` through `hv6`   | helper variable registers                 | helper variables for some arithmetic operations                                                                                                                                                                           |
 | *`ramp`                | RAM pointer                               | contains an address pointing into the RAM                                                                                                                                                                                 |
 | *`ramv`                | RAM value                                 | contains the value of the RAM element at the address currently held in `ramp`                                                                                                                                             |