fix(doc): correct explanations for previous designs

TritonVM · Oct 25, 2023 · 4bbc2d2 · 4bbc2d2
1 parent 308d67f
commit 4bbc2d2
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 7 deletions.
diff --git a/specification/src/contiguity-of-memory-pointer-regions.md b/specification/src/contiguity-of-memory-pointer-regions.md
@@ -2,10 +2,12 @@
 
 ## Contiguity for Op Stack Table
 
-In each cycle, the memory pointer for the Op Stack 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 Jump Stack Table
 
@@ -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.
diff --git a/specification/src/registers.md b/specification/src/registers.md
@@ -17,7 +17,7 @@ the remaining registers exist only to enable an efficient arithmetization and ar
 | `jso`                  | jump stack origin                         | contains the value of the instruction pointer of the last `call`                                                                                                                                                          |
 | `jsd`                  | jump stack destination                    | contains the argument of the last `call`                                                                                                                                                                                  |
 | `st0` through `st15`   | operational stack registers               | contain explicit operational stack values                                                                                                                                                                                 |
-| *`osp`                 | operational stack pointer                 | contains the op stack address of the top of the operational stack                                                                                                                                                         |
+| *`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                                                                                                                                                                                 |
@@ -40,11 +40,14 @@ In order to access elements of the op stack held in op stack underflow memory, t
 The stack grows upwards, in line with the metaphor that justifies the name "stack".
 
 For reasons of arithmetization, the stack always contains a minimum of 16 elements.
-All these elements are initially 0.
 Trying to run an instruction which would result in a stack of smaller total length than 16 crashes the VM.
 
-The registers `osp` and `osv` are not directly accessible by the program running in TritonVM.
-They exist only to allow efficient arithmetization.
+Stack elements `st0` through `st10` are initially 0.
+Stack elements `st11` through `st15`, _i.e._, the very bottom of the stack, are initialized with the hash digest of the program that is being executed.
+See [the mechanics of program attestation](program-attestation.md#mechanics) for further explanations on stack initialization.
+
+The register `op_stack_pointer` is not directly accessible by the program running in TritonVM.
+It exists only to allow efficient arithmetization.
 
 ## RAM