diff --git a/assets/design/decoder/decoder_dyn_operation.png b/assets/design/decoder/decoder_dyn_operation.png index 93426e0d3..71da6f13a 100644 Binary files a/assets/design/decoder/decoder_dyn_operation.png and b/assets/design/decoder/decoder_dyn_operation.png differ diff --git a/assets/design/decoder/decoder_dyncall_operation.png b/assets/design/decoder/decoder_dyncall_operation.png new file mode 100644 index 000000000..2c0effc4d Binary files /dev/null and b/assets/design/decoder/decoder_dyncall_operation.png differ diff --git a/design/decoder/constraints.html b/design/decoder/constraints.html index d38367a50..32714e87a 100644 --- a/design/decoder/constraints.html +++ b/design/decoder/constraints.html @@ -333,18 +333,23 @@

refers to a column in the decoder, as depicted. The addresses in this column are set using the address from the hasher chiplet for the corresponding hash initialization / absorption / return. In the case of the value of the address in column in the current row of the decoder is set to equal the value of the address of the row in the hasher chiplet where the previous absorption (or initialization) occurred. is the address of the next row of the decoder, which is set to equal the address in the hasher chiplet where the absorption referred to by the label is happening.

In the above, represents the address value in the decoder which corresponds to the hasher chiplet address at which the hasher was initialized (or the last absorption took place). As such, corresponds to the hasher chiplet address at which the result is returned.

-

-

In the above, is set to when a control flow operation that signifies the initialization of a control block is being executed on the VM. Otherwise, it is set to . An exception is made for the SYSCALL operation. Although it also signifies the initialization of a control block, it must additionally send a procedure access request to the kernel ROM chiplet via the chiplets bus. Therefore, it is excluded from this flag and its communication with the chiplets bus is handled separately.

+

+

In the above, is set to when a control flow operation that signifies the initialization of a control block is being executed on the VM (only those control blocks that don't do any concurrent requests to the chiplets but). Otherwise, it is set to . An exception is made for the DYN, DYNCALL, and SYSCALL operations, since although they initialize a control block, they also run another concurrent bus request, and so are handled separately.

In the above, represents the opcode value of the opcode being executed on the virtual machine. It is calculated via a bitwise combination of the op bits. We leverage the opcode value to achieve domain separation when hashing control blocks. This is done by populating the second capacity register of the hasher with the value via the term when initializing the hasher.

Using the above variables, we define operation values as described below.

-

When a control block initializer operation (JOIN, SPLIT, LOOP, DYN, CALL, SYSCALL) is executed, a new hasher is initialized and the contents of are absorbed into the hasher. As mentioned above, the opcode value is populated in the second capacity resister via the term.

+

When a control block initializer operation (JOIN, SPLIT, LOOP, CALL) is executed, a new hasher is initialized and the contents of are absorbed into the hasher. As mentioned above, the opcode value is populated in the second capacity register via the term.

As mentioned previously, the value sent by the SYSCALL operation is defined separately, since in addition to communicating with the hash chiplet it must also send a kernel procedure access request to the kernel ROM chiplet. This value of this kernel procedure request is described by .

In the above, is the unique operation label of the kernel procedure call operation. The values contain the root hash of the procedure being called, which is the procedure that must be requested from the kernel ROM chiplet.

The above value sends both the hash initialization request and the kernel procedure access request to the chiplets bus when the SYSCALL operation is executed.

+

Similar to SYSCALL, DYN and DYNCALL are handled separately, since in addition to communicating with the hash chiplet they must also issue a memory read operation for the hash of the procedure being called.

+

+

+

+

In the above, can be thought of as , but where the values used for the hasher decoder trace registers is all 0's. represents a memory read request from memory address (the top stack element), where the result is placed in the first half of the decoder hasher trace, and where is a label that represents a memory read request.

When SPAN operation is executed, a new hasher is initialized and contents of are absorbed into the hasher. The number of operation groups to be hashed is padded to a multiple of the rate width () and so the is set to 0:

When RESPAN operation is executed, contents of (which contain the new operation batch) are absorbed into the hasher:

@@ -353,7 +358,7 @@

Using the above definitions, we can describe the constraint for computing block hashes as follows:

-

+

We need to add and subtract the sum of the relevant operation flags to ensure that when none of the flags is set to , the above constraint reduces to .

The degree of this constraint is .

@@ -381,13 +386,15 @@

When a DYN operation is executed, row is added to the block stack table:

-

When a CALL or SYSCALL operation is executed, row is added to the block stack table:

-

-

When END operation is executed, how we construct the row will depend on whether the IS_CALL or IS_SYSCALL values are set (stored in registers and respectively). If they are not set, then row is removed from the block span table (where contains the is_loop flag); otherwise, row .

-

+

When a DYNCALL operation is executed, row is added to the block stack table:

+

+

When a CALL or SYSCALL operation is executed, row is added to the block stack table:

+

+

When END operation is executed, how we construct the row will depend on whether the IS_CALL or IS_SYSCALL values are set (stored in registers and respectively). If they are not set, then row is removed from the block span table (where contains the is_loop flag); otherwise, row .

+

Using the above definitions, we can describe the constraint for updating the block stack table as follows:

-

+

We need to add and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to , the above constraint reduces to .

The degree of this constraint is .

@@ -415,16 +422,13 @@

When REPEAT operation is executed, hash of loop body is added to the block hash table. We add term to indicate that the child is a body of a loop:

-

When the DYN operation is executed, the hash of the dynamic child is added to the block hash table. Since the child is dynamically specified by the top four elements of the stack, the value representing the dyn block's child must be computed based on the stack rather than from the decoder's hasher registers:

-

-

-

When the CALL or SYSCALL operation is executed, the hash of the callee is added to the block hash table.

-

+

When DYN, DYNCALL, CALL or SYSCALL operation is executed, the hash of the child is added to the block hash table. In all cases, this child is found in the first half of the decoder hasher state.

+

When END operation is executed, hash of the completed block is removed from the block hash table. However, we also need to differentiate between removing the first and the second child of a join block. We do this by looking at the next operation. Specifically, if the next operation is neither END nor REPEAT nor HALT, we know that another block is about to be executed, and thus, we have just finished executing the first child of a join block. Thus, if the next operation is neither END nor REPEAT nor HALT we need to set the term for coefficient to as shown below:

Using the above definitions, we can describe the constraint for updating the block hash table as follows:

-

+

We need to add and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to , the above constraint reduces to .

The degree of this constraint is .

diff --git a/design/decoder/main.html b/design/decoder/main.html index 8aeea4b0f..3827f5c38 100644 --- a/design/decoder/main.html +++ b/design/decoder/main.html @@ -485,16 +485,37 @@

SPAN operation<
  • Sets the op_index register to .

    • DYN operation

    -

    Before a DYN operation is executed by the VM, the prover populates registers with as shown in the diagram below.

    decoder_dyn_operation

    -

    In the above diagram, blk is the ID of the dyn block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. prnt is the ID of the block's parent.

    +

    In the above diagram, blk is the ID of the dyn block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. p_addr is the ID of the block's parent.

    When the VM executes a DYN operation, it does the following:

      -
    1. Adds a tuple (blk, prnt, 0, 0...) to the block stack table.
      2. -
    2. Gets the hash of the dynamic code block dynamic_block_hash from the top four elements of the stack.
      3. -
    3. Adds the tuple (blk, dynamic_block_hash, 0, 0) to the block hash table.
      4. -
    4. Initiates a 2-to-1 hash computation in the hash chiplet (as described here) using blk as row address in the auxiliary hashing table and as input values.
      5. +
    5. Adds a tuple (blk, p_addr, 0, 0...) to the block stack table.
      6. +
    6. Sends a memory read request to the memory chiplet, using s0 as the memory address. The result hash of callee is placed in the decoder hasher trace at .
      7. +
    7. Adds the tuple (blk, hash of callee, 0, 0) to the block hash table.
      8. +
    8. Initiates a 2-to-1 hash computation in the hash chiplet (as described here) using blk as row address in the auxiliary hashing table and [ZERO; 8] as input values.
      9. +
    9. Performs a stack left shift +
        +
      • Above s16 was pulled from the stack overflow table if present; otherwise set to 0.
        • +
      +
      10. +
    +

    Note that unlike DYNCALL, the fmp, ctx, in_syscall and fn_hash registers are unchanged.

    +

    DYNCALL operation

    +

    decoder_dyncall_operation

    +

    In the above diagram, blk is the ID of the dyn block which is about to be executed. blk is also the address of the hasher row in the auxiliary hasher table. p_addr is the ID of the block's parent.

    +

    When the VM executes a DYNCALL operation, it does the following:

    +
      +
    1. Adds a tuple (blk, p_addr, 0, ctx, fmp, b_0, b_1, fn_hash[0..3]) to the block stack table.
      2. +
    2. Sends a memory read request to the memory chiplet, using s0 as the memory address. The result hash of callee is placed in the decoder hasher trace at .
      3. +
    3. Adds the tuple (blk, hash of callee, 0, 0) to the block hash table.
      4. +
    4. Initiates a 2-to-1 hash computation in the hash chiplet (as described here) using blk as row address in the auxiliary hashing table and [ZERO; 8] as input values.
      5. +
    5. Performs a stack left shift +
        +
      • Above s16 was pulled from the stack overflow table if present; otherwise set to 0.
        • +
      +
    +

    Similar to CALL, DYNCALL resets the fmp, sets up a new ctx, and sets the fn_hash registers to the callee hash. in_syscall needs to be 0, since calls are not allowed during a syscall.

    END operation

    Before an END operation is executed by the VM, the prover populates registers with the hash of the block which is about to end. The prover also sets values in and registers as follows: