Stack operation constraints

In addition to the constraints described in the previous section, we need to impose constraints to check that each VM operation is executed correctly.

For this purpose the VM exposes a set of operation-specific flags. These flags are set to when a given operation is executed, and to otherwise. The naming convention for these flags is . For example, would be set to when DUP operation is executed, and to otherwise. Operation flags are discussed in detail in the section below.

To describe how operation-specific constraints work, let's use an example with DUP operation. This operation pushes a copy of the top stack item onto the stack. The constraints we need to impose for this operation are as follows:

The first constraint enforces that the top stack item in the next row is the same as the top stack item in the current row. The second constraint enforces that all stack items (starting from item ) are shifted to the right by . We also need to impose all the constraints discussed in the previous section, be we omit them here.

Let's write similar constraints for DUP1 operation, which pushes a copy of the second stack item onto the stack:

It is easy to notice that while the first constraint changed, the second constraint remained the same - i.e., we are still just shifting the stack to the right.

In fact, for most operations it makes sense to make a distinction between constraints unique to the operation vs. more general constraints which enforce correct behavior for the stack items not affected by the operation. In the subsequent sections we describe in detail only the former constraints, and provide high-level descriptions of the more general constraints. Specifically, we indicate how the operation affects the rest of the stack (e.g., shifts right starting from position ).

Operation flags

As mentioned above, operation flags are used as selectors to enforce operation-specific constraints. That is, they turn on relevant constraints for a given operation. In total, the VM provides unique operations, and thus, there are operation flags (not all of them currently used).

Operation flags are mutually exclusive. That is, if one flag is set to , all other flags are set to . Also, one of the flags is always guaranteed to be set to .

To compute values of operation flags we use op bits registers located in the decoder. These registers contain binary representations of operation codes (opcodes). Each opcode consists of bits, and thus, there are op bits registers. We denote these registers as . The values are computed by multiplying the op bit registers in various combinations. Notice that binary encoding down below is showed in big-endian order, so the flag bits correspond to the reverse order of the op bits registers, from to .

For example, the value of the flag for NOOP, which is encoded as 0000000, is computed as follows:

While the value of the DROP operation, which is encoded as 0101001 is computed as follows:

As can be seen from above, the degree for both of these flags is . Since degree of constraints in Miden VM can go up to , this means that operation-specific constraints cannot exceed degree . However, there are some operations which require constraints of higher degree (e.g., or even ). To support such constraints, we adopt the following scheme.

We organize the operations into groups as shown below and also introduce two extra registers and for degree reduction:

# of opsdegree
0xxxxxx00647
100xxx-0086
101xxxx10165
11xxx--0184

In the above:

  • Operation flags for operations in the first group (with prefix 0), are computed using all op bits, and thus their degree is .
  • Operation flags for operations in the second group (with prefix 100), are computed using only the first op bits, and thus their degree is .
  • Operation flags for operations in the third group (with prefix 101), are computed using all op bits. We use the extra register (which is set to ) to reduce the degree by . Thus, the degree of op flags in this group is .
  • Operation flags for operations in the fourth group (with prefix 11), are computed using only the first op bits. We use the extra register (which is set to ) to reduce the degree by . Thus, the degree of op flags in this group is .

How operations are distributed between these groups is described in the sections below.

No stack shift operations

This group contains operations which do not shift the stack (this is almost all such operations). Since the op flag degree for these operations is , constraints for these operations cannot exceed degree .

OperationOpcode valueBinary encodingOperation groupFlag degree
NOOP000_0000System ops
EQZ 000_0001Field ops
NEG000_0010Field ops
INV000_0011Field ops
INCR000_0100Field ops
NOT000_0101Field ops
FMPADD000_0110System ops
MLOAD000_0111I/O ops
SWAP000_1000Stack ops
CALLER000_1001System ops
MOVUP2000_1010Stack ops
MOVDN2000_1011Stack ops
MOVUP3000_1100Stack ops
MOVDN3000_1101Stack ops
ADVPOPW000_1110I/O ops
EXPACC000_1111Field ops
MOVUP4001_0000Stack ops
MOVDN4001_0001Stack ops
MOVUP5001_0010Stack ops
MOVDN5001_0011Stack ops
MOVUP6001_0100Stack ops
MOVDN6001_0101Stack ops
MOVUP7001_0110Stack ops
MOVDN7001_0111Stack ops
SWAPW001_1000Stack ops
EXT2MUL001_1001Field ops
MOVUP8001_1010Stack ops
MOVDN8001_1011Stack ops
SWAPW2001_1100Stack ops
SWAPW3001_1101Stack ops
SWAPDW001_1110Stack ops
<unused>001_1111

Left stack shift operations

This group contains operations which shift the stack to the left (i.e., remove an item from the stack). Most of left-shift operations are contained in this group. Since the op flag degree for these operations is , constraints for these operations cannot exceed degree .

OperationOpcode valueBinary encodingOperation groupFlag degree
ASSERT010_0000System ops
EQ010_0001Field ops
ADD010_0010Field ops
MUL010_0011Field ops
AND010_0100Field ops
OR010_0101Field ops
U32AND010_0110u32 ops
U32XOR010_0111u32 ops
FRIE2F4010_1000Crypto ops
DROP010_1001Stack ops
CSWAP010_1010Stack ops
CSWAPW010_1011Stack ops
MLOADW010_1100I/O ops
MSTORE010_1101I/O ops
MSTOREW010_1110I/O ops
FMPUPDATE010_1111System ops

Right stack shift operations

This group contains operations which shift the stack to the right (i.e., push a new item onto the stack). Most of right-shift operations are contained in this group. Since the op flag degree for these operations is , constraints for these operations cannot exceed degree .

OperationOpcode valueBinary encodingOperation groupFlag degree
PAD011_0000Stack ops
DUP011_0001Stack ops
DUP1011_0010Stack ops
DUP2011_0011Stack ops
DUP3011_0100Stack ops
DUP4011_0101Stack ops
DUP5011_0110Stack ops
DUP6011_0111Stack ops
DUP7011_1000Stack ops
DUP9011_1001Stack ops
DUP11011_1010Stack ops
DUP13011_1011Stack ops
DUP15011_1100Stack ops
ADVPOP011_1101I/O ops
SDEPTH011_1110I/O ops
CLK011_1111System ops

u32 operations

This group contains u32 operations. These operations are grouped together because all of them require range checks. The constraints for range checks are of degree , however, since all these operations require them, we can define a flag with common prefix 100 to serve as a selector for the range check constraints. The value of this flag is computed as follows:

The degree of this flag is , which is acceptable for a selector for degree constraints.

OperationOpcode valueBinary encodingOperation groupFlag degree
U32ADD100_0000u32 ops
U32SUB100_0010u32 ops
U32MUL100_0100u32 ops
U32DIV100_0110u32 ops
U32SPLIT100_1000u32 ops
U32ASSERT2100_1010u32 ops
U32ADD3100_1100u32 ops
U32MADD100_1110u32 ops

As mentioned previously, the last bit of the opcode is not used in computation of the flag for these operations. We force this bit to always be set to with the following constraint:

Putting these operations into a group with flag degree is important for two other reasons:

  • Constraints for the U32SPLIT operation have degree . Thus, the degree of the op flag for this operation cannot exceed .
  • Operations U32ADD3 and U32MADD shift the stack to the left. Thus, having these two operations in this group and putting them under the common prefix 10011 allows us to create a common flag for these operations of degree (recall that the left-shift flag cannot exceed degree ).

High-degree operations

This group contains operations which require constraints with degree up to . All operation bits are used for these flags. The extra column is used for degree reduction of the three high-degree bits.

OperationOpcode valueBinary encodingOperation groupFlag degree
HPERM101_0000Crypto ops
MPVERIFY101_0001Crypto ops
PIPE101_0010I/O ops
MSTREAM101_0011I/O ops
SPLIT101_0100Flow control ops
LOOP101_0101Flow control ops
SPAN101_0110Flow control ops
JOIN101_0111Flow control ops
DYN101_1000Flow control ops
RCOMBBASE101_1001Crypto ops
<unused>101_1010
<unused>101_1011
<unused>101_1100
<unused>101_1101
<unused>101_1110
<unused>101_1111

Note that the SPLIT and LOOP operations are grouped together under the common prefix 101010, and thus can have a common flag of degree (using for degree reduction). This is important because both of these operations shift the stack to the left.

Also, we need to make sure that extra register , which is used to reduce the flag degree by , is set to when , , and :

Very high-degree operations

This group contains operations which require constraints with degree up to .

OperationOpcode valueBinary encodingOperation groupFlag degree
MRUPDATE110_0000Crypto ops
PUSH110_0100I/O ops
SYSCALL110_1000Flow control ops
CALL110_1100Flow control ops
END111_0000Flow control ops
REPEAT111_0100Flow control ops
RESPAN111_1000Flow control ops
HALT111_1100Flow control ops

As mentioned previously, the last two bits of the opcode are not used in computation of the flag for these operations. We force these bits to always be set to with the following constraints:

Also, we need to make sure that extra register , which is used to reduce the flag degree by , is set to when both and columns are set to :

Composite flags

Using the operation flags defined above, we can compute several composite flags which are used by various constraints in the VM.

Shift right flag

The right-shift flag indicates that an operation shifts the stack to the right. This flag is computed as follows:

In the above, evaluates to for all right stack shift operations described previously. This works because all these operations have a common prefix 011. We also need to add in flags for other operations which shift the stack to the right but are not a part of the above group (e.g., PUSH operation).

Shift left flag

The left-shift flag indicates that a given operation shifts the stack to the left. To simplify the description of this flag, we will first compute the following intermediate variables:

A flag which is set to when or :

A flag which is set to when or :

Using the above variables, we compute left-shift flag as follows:

In the above:

  • evaluates to for all left stack shift operations described previously. This works because all these operations have a common prefix 010.
  • is the helper register in the decoder which is set to when we are exiting a LOOP block, and to otherwise.

Thus, similarly to the right-shift flag, we compute the value of the left-shift flag based on the prefix of the operation group which contains most left shift operations, and add in flag values for other operations which shift the stack to the left but are not a part of this group.

Control flow flag

The control flow flag is set to when a control flow operation is being executed by the VM, and to otherwise. Naively, this flag can be computed as follows:

However, this can be computed more efficiently via the common operation prefixes for the two groups of control flow operations as follows.