u32 Operations

Miden assembly provides a set of instructions which can perform operations on regular two-complement 32-bit integers. These instructions are described in the tables below.

For instructions where one or more operands can be provided as immediate parameters (e.g., u32wrapping_add and u32wrapping_add.b), we provide stack transition diagrams only for the non-immediate version. For the immediate version, it can be assumed that the operand with the specified name is not present on the stack.

In all the table below, the number of cycles it takes for the VM to execute each instruction is listed beneath the instruction.

Notes on Undefined Behavior

Most of the instructions documented below expect to receive operands whose values are valid u32 values, i.e. values in the range $0.. = (2^{32} - 1)$ . Currently, the semantics of the instructions when given values outside of that range are undefined (as noted in the documented semantics for each instruction). The rule with undefined behavior generally speaking is that you can make no assumptions about what will happen if your program exhibits it.

For purposes of describing the effects of undefined behavior below, we will refer to values which are not valid for the input type of the affected operation, e.g. u32, as poison. Any use of a poison value propagates the poison state. For example, performing u32div with a poison operand, can be considered as producing a poison value as its result, for the purposes of discussing undefined behavior semantics.

With that in mind, there are two ways in which the effects of undefined behavior manifest:

Executor Semantics

From an executor perspective, currently, the semantics are completely undefined. An executor can do everything from terminate the program, panic, always produce 42 as a result, produce a random result, or something more principled.

In practice, the Miden VM, when executing an operation, will almost always trap on poison values. This is not guaranteed, but is currently the case for most operations which have niches of undefined behavior. To the extent that some other behavior may occur, it will generally be to truncate/wrap the poison value, but this is subject to change at any time, and is undocumented. You should assume that all operations will trap on poison.

The reason the Miden VM makes the choice to trap on poison, is to ensure that undefined behavior is caught close to the source, rather than propagated silently throughout the program. It also has the effect of ensuring you do not execute a program with undefined behavior, and produce a proof that is not actually valid, as we will describe in a moment.

Verifier Semantics

From the perspective of the verifier, the implementation details of the executor are completely unknown. For example, the fact that the Miden VM traps on poison values is not actually verified by constraints. An alternative executor implementation could choose not to trap, and thus appear to execute successfully. The resulting proof, however, as a result of the program exhibiting undefined behavior, is not a valid proof. In effect the use of poison values "poisons" the proof as well.

As a result, a program that exhibits undefined behavior, and executes successfully, will produce a proof that could pass verification, even though it should not. In other words, the proof does not prove what it says it does.

In the future, we may attempt to remove niches of undefined behavior in such a way that producing such invalid proofs is not possible, but for the time being, you must ensure that your program does not exhibit (or rely on) undefined behavior.

Conversions and tests

Instruction	Stack_input	Stack_output	Notes
u32test - (5 cycles)	[a, ...]	[b, a, ...]	$b \leftarrow {1, 0, if a < 2^{32} otherwise$
u32testw - (23 cycles)	[A, ...]	[b, A, ...]	$b \leftarrow {1, 0, if \forall i \in {0, 1, 2, 3} a_{i} < 2^{32} otherwise$
u32assert - (3 cycles)	[a, ...]	[a, ...]	Fails if $a \geq 2^{32}$
u32assert2 - (1 cycle)	[b, a,...]	[b, a,...]	Fails if $a \geq 2^{32}$ or $b \geq 2^{32}$
u32assertw - (6 cycles)	[A, ...]	[A, ...]	Fails if $\exists i \in {0, 1, 2, 3} : a_{i} \geq 2^{32}$
u32cast - (2 cycles)	[a, ...]	[b, ...]	$b \leftarrow a mod 2^{32}$
u32split - (1 cycle)	[a, ...]	[c, b, ...]	$b \leftarrow a mod 2^{32}$ , $c \leftarrow ⌊ a / 2^{32} ⌋$

The instructions u32assert, u32assert2 and u32assertw can also be parametrized with an error code which can be any 32-bit value specified either directly or via a named constant. For example:

u32assert.err=123
u32assert.err=MY_CONSTANT

If the error code is omitted, the default value of $0$ is assumed.

Arithmetic operations

Instruction	Stack_input	Stack_output	Notes
u32overflowing_add - (1 cycle) u32overflowing_add.b - (2-3 cycles)	[b, a, ...]	[d, c, ...]	$c \leftarrow (a + b) mod 2^{32}$ $d \leftarrow {1, 0, if (a + b) \geq 2^{32} otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32wrapping_add - (2 cycles) u32wrapping_add.b - (3-4 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow (a + b) mod 2^{32}$ Undefined if $ma x (a, b) \geq 2^{32}$
u32overflowing_add3 - (1 cycle)	[c, b, a, ...]	[e, d, ...]	$d \leftarrow (a + b + c) mod 2^{32}$ , $e \leftarrow ⌊(a + b + c) / 2^{32} ⌋$ Undefined if $ma x (a, b, c) \geq 2^{32}$
u32wrapping_add3 - (2 cycles)	[c, b, a, ...]	[d, ...]	$d \leftarrow (a + b + c) mod 2^{32}$ , Undefined if $ma x (a, b, c) \geq 2^{32}$
u32overflowing_sub - (1 cycle) u32overflowing_sub.b - (2-3 cycles)	[b, a, ...]	[d, c, ...]	$c \leftarrow (a - b) mod 2^{32}$ $d \leftarrow {1, 0, if a < b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32wrapping_sub - (2 cycles) u32wrapping_sub.b - (3-4 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow (a - b) mod 2^{32}$ Undefined if $ma x (a, b) \geq 2^{32}$
u32overflowing_mul - (1 cycle) u32overflowing_mul.b - (2-3 cycles)	[b, a, ...]	[d, c, ...]	$c \leftarrow (a \cdot b) mod 2^{32}$ $d \leftarrow ⌊(a \cdot b) / 2^{32} ⌋$ Undefined if $ma x (a, b) \geq 2^{32}$
u32wrapping_mul - (2 cycles) u32wrapping_mul.b - (3-4 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow (a \cdot b) mod 2^{32}$ Undefined if $ma x (a, b) \geq 2^{32}$
u32overflowing_madd - (1 cycle)	[b, a, c, ...]	[e, d, ...]	$d \leftarrow (a \cdot b + c) mod 2^{32}$ $e \leftarrow ⌊(a \cdot b + c) / 2^{32} ⌋$ Undefined if $ma x (a, b, c) \geq 2^{32}$
u32wrapping_madd - (2 cycles)	[b, a, c, ...]	[d, ...]	$d \leftarrow (a \cdot b + c) mod 2^{32}$ Undefined if $ma x (a, b, c) \geq 2^{32}$
u32div - (2 cycles) u32div.b - (3-4 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow ⌊ a / b ⌋$ Fails if $b = 0$ Undefined if $ma x (a, b) \geq 2^{32}$
u32mod - (3 cycles) u32mod.b - (4-5 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow a mod b$ Fails if $b = 0$ Undefined if $ma x (a, b) \geq 2^{32}$
u32divmod - (1 cycle) u32divmod.b - (2-3 cycles)	[b, a, ...]	[d, c, ...]	$c \leftarrow ⌊ a / b ⌋$ $d \leftarrow a mod b$ Fails if $b = 0$ Undefined if $ma x (a, b) \geq 2^{32}$

Bitwise operations

Instruction	Stack_input	Stack_output	Notes
u32and - (1 cycle) u32and.b - (2 cycles)	[b, a, ...]	[c, ...]	Computes $c$ as a bitwise `AND` of binary representations of $a$ and $b$ . Fails if $ma x (a, b) \geq 2^{32}$
u32or - (6 cycle)s u32or.b - (7 cycles)	[b, a, ...]	[c, ...]	Computes $c$ as a bitwise `OR` of binary representations of $a$ and $b$ . Fails if $ma x (a, b) \geq 2^{32}$
u32xor - (1 cycle) u32xor.b - (2 cycles)	[b, a, ...]	[c, ...]	Computes $c$ as a bitwise `XOR` of binary representations of $a$ and $b$ . Fails if $ma x (a, b) \geq 2^{32}$
u32not - (5 cycles) u32not.a - (6 cycles)	[a, ...]	[b, ...]	Computes $b$ as a bitwise `NOT` of binary representation of $a$ . Fails if $a \geq 2^{32}$
u32shl - (18 cycles) u32shl.b - (3 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow (a \cdot 2^{b}) mod 2^{32}$ Undefined if $a \geq 2^{32}$ or $b > 31$
u32shr - (18 cycles) u32shr.b - (3 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow ⌊ a / 2^{b} ⌋$ Undefined if $a \geq 2^{32}$ or $b > 31$
u32rotl - (18 cycles) u32rotl.b - (3 cycles)	[b, a, ...]	[c, ...]	Computes $c$ by rotating a 32-bit representation of $a$ to the left by $b$ bits. Undefined if $a \geq 2^{32}$ or $b > 31$
u32rotr - (23 cycles) u32rotr.b - (3 cycles)	[b, a, ...]	[c, ...]	Computes $c$ by rotating a 32-bit representation of $a$ to the right by $b$ bits. Undefined if $a \geq 2^{32}$ or $b > 31$
u32popcnt - (33 cycles)	[a, ...]	[b, ...]	Computes $b$ by counting the number of set bits in $a$ (hamming weight of $a$ ). Undefined if $a \geq 2^{32}$
u32clz - (42 cycles)	[a, ...]	[b, ...]	Computes $b$ as a number of leading zeros of $a$ . Undefined if $a \geq 2^{32}$
u32ctz - (34 cycles)	[a, ...]	[b, ...]	Computes $b$ as a number of trailing zeros of $a$ . Undefined if $a \geq 2^{32}$
u32clo - (41 cycles)	[a, ...]	[b, ...]	Computes $b$ as a number of leading ones of $a$ . Undefined if $a \geq 2^{32}$
u32cto - (33 cycles)	[a, ...]	[b, ...]	Computes $b$ as a number of trailing ones of $a$ . Undefined if $a \geq 2^{32}$

Comparison operations

Instruction	Stack_input	Stack_output	Notes
u32lt - (3 cycles) u32lt.b - (4 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow {1, 0, if a < b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32lte - (5 cycles) u32lte.b - (6 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow {1, 0, if a \leq b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32gt - (4 cycles) u32gt.b - (5 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow {1, 0, if a > b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32gte - (4 cycles) u32gte.b - (5 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow {1, 0, if a \geq b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32min - (8 cycles) u32min.b - (9 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow {a, b, if a < b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$
u32max - (9 cycles) u32max.b - (10 cycles)	[b, a, ...]	[c, ...]	$c \leftarrow {a, b, if a > b otherwise$ Undefined if $ma x (a, b) \geq 2^{32}$