From 4bbc2d2a32101f518ef1a9bd96f5c7c8a3cfa576 Mon Sep 17 00:00:00 2001 From: Jan Ferdinand Sauer Date: Wed, 25 Oct 2023 11:17:26 +0200 Subject: [PATCH] fix(doc): correct explanations for previous designs --- .../src/contiguity-of-memory-pointer-regions.md | 12 +++++++++--- specification/src/registers.md | 11 +++++++---- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/specification/src/contiguity-of-memory-pointer-regions.md b/specification/src/contiguity-of-memory-pointer-regions.md index 877c5b47e..fd280b062 100644 --- 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 index 721644849..9860f061c 100644 --- 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