## 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←{1,0, ifa<2_{32}otherwise $ |

u32testw - (23 cycles) | [A, ...] | [b, A, ...] | $b←{1,0, if∀i∈{0,1,2,3}a_{i}<2_{32}otherwise $ |

u32assert - (3 cycles) | [a, ...] | [a, ...] | Fails if $a≥2_{32}$ |

u32assert2 - (1 cycle) | [b, a,...] | [b, a,...] | Fails if $a≥2_{32}$ or $b≥2_{32}$ |

u32assertw - (6 cycles) | [A, ...] | [A, ...] | Fails if $∃i∈{0,1,2,3}:a_{i}≥2_{32}$ |

u32cast - (2 cycles) | [a, ...] | [b, ...] | $b←amod2_{32}$ |

u32split - (1 cycle) | [a, ...] | [c, b, ...] | $b←amod2_{32}$, $c←⌊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←(a+b)mod2_{32}$ $d←{1,0, if(a+b)≥2_{32}otherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32wrapping_add - (2 cycles) u32wrapping_add. b - (3-4 cycles) | [b, a, ...] | [c, ...] | $c←(a+b)mod2_{32}$ Undefined if $max(a,b)≥2_{32}$ |

u32overflowing_add3 - (1 cycle) | [c, b, a, ...] | [e, d, ...] | $d←(a+b+c)mod2_{32}$, $e←⌊(a+b+c)/2_{32}⌋$ Undefined if $max(a,b,c)≥2_{32}$ |

u32wrapping_add3 - (2 cycles) | [c, b, a, ...] | [d, ...] | $d←(a+b+c)mod2_{32}$, Undefined if $max(a,b,c)≥2_{32}$ |

u32overflowing_sub - (1 cycle) u32overflowing_sub. b - (2-3 cycles) | [b, a, ...] | [d, c, ...] | $c←(a−b)mod2_{32}$ $d←{1,0, ifa<botherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32wrapping_sub - (2 cycles) u32wrapping_sub. b - (3-4 cycles) | [b, a, ...] | [c, ...] | $c←(a−b)mod2_{32}$ Undefined if $max(a,b)≥2_{32}$ |

u32overflowing_mul - (1 cycle) u32overflowing_mul. b - (2-3 cycles) | [b, a, ...] | [d, c, ...] | $c←(a⋅b)mod2_{32}$ $d←⌊(a⋅b)/2_{32}⌋$ Undefined if $max(a,b)≥2_{32}$ |

u32wrapping_mul - (2 cycles) u32wrapping_mul. b - (3-4 cycles) | [b, a, ...] | [c, ...] | $c←(a⋅b)mod2_{32}$ Undefined if $max(a,b)≥2_{32}$ |

u32overflowing_madd - (1 cycle) | [b, a, c, ...] | [e, d, ...] | $d←(a⋅b+c)mod2_{32}$ $e←⌊(a⋅b+c)/2_{32}⌋$ Undefined if $max(a,b,c)≥2_{32}$ |

u32wrapping_madd - (2 cycles) | [b, a, c, ...] | [d, ...] | $d←(a⋅b+c)mod2_{32}$ Undefined if $max(a,b,c)≥2_{32}$ |

u32div - (2 cycles) u32div. b - (3-4 cycles) | [b, a, ...] | [c, ...] | $c←⌊a/b⌋$ Fails if $b=0$ Undefined if $max(a,b)≥2_{32}$ |

u32mod - (3 cycles) u32mod. b - (4-5 cycles) | [b, a, ...] | [c, ...] | $c←amodb$ Fails if $b=0$ Undefined if $max(a,b)≥2_{32}$ |

u32divmod - (1 cycle) u32divmod. b - (2-3 cycles) | [b, a, ...] | [d, c, ...] | $c←⌊a/b⌋$ $d←amodb$ Fails if $b=0$ Undefined if $max(a,b)≥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 $max(a,b)≥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 $max(a,b)≥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 $max(a,b)≥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≥2_{32}$ |

u32shl - (18 cycles) u32shl. b - (3 cycles) | [b, a, ...] | [c, ...] | $c←(a⋅2_{b})mod2_{32}$ Undefined if $a≥2_{32}$ or $b>31$ |

u32shr - (18 cycles) u32shr. b - (3 cycles) | [b, a, ...] | [c, ...] | $c←⌊a/2_{b}⌋$ Undefined if $a≥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≥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≥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≥2_{32}$ |

u32clz - (42 cycles) | [a, ...] | [b, ...] | Computes $b$ as a number of leading zeros of $a$. Undefined if $a≥2_{32}$ |

u32ctz - (34 cycles) | [a, ...] | [b, ...] | Computes $b$ as a number of trailing zeros of $a$. Undefined if $a≥2_{32}$ |

u32clo - (41 cycles) | [a, ...] | [b, ...] | Computes $b$ as a number of leading ones of $a$. Undefined if $a≥2_{32}$ |

u32cto - (33 cycles) | [a, ...] | [b, ...] | Computes $b$ as a number of trailing ones of $a$. Undefined if $a≥2_{32}$ |

### Comparison operations

Instruction | Stack_input | Stack_output | Notes |
---|---|---|---|

u32lt - (3 cycles) u32lt. b - (4 cycles) | [b, a, ...] | [c, ...] | $c←{1,0, ifa<botherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32lte - (5 cycles) u32lte. b - (6 cycles) | [b, a, ...] | [c, ...] | $c←{1,0, ifa≤botherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32gt - (4 cycles) u32gt. b - (5 cycles) | [b, a, ...] | [c, ...] | $c←{1,0, ifa>botherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32gte - (4 cycles) u32gte. b - (5 cycles) | [b, a, ...] | [c, ...] | $c←{1,0, ifa≥botherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32min - (8 cycles) u32min. b - (9 cycles) | [b, a, ...] | [c, ...] | $c←{a,b, ifa<botherwise $ Undefined if $max(a,b)≥2_{32}$ |

u32max - (9 cycles) u32max. b - (10 cycles) | [b, a, ...] | [c, ...] | $c←{a,b, ifa>botherwise $ Undefined if $max(a,b)≥2_{32}$ |