u32 Operations

In this section we describe semantics and AIR constraints of operations over u32 values (i.e., 32-bit unsigned integers) as they are implemented in Miden VM. Unless stated otherwise, $s_0$ denotes the top of the stack, $s_1$ the next element, $s_2$ the third element, and so on.

Range checks

Most operations described below require some number of 16-bit range checks (i.e., verifying that the value of a field element is smaller than $2^{16}$). The number of required range checks varies between $2$ and $4$, depending on the operation. However, to simplify the constraint system, we force each relevant operation to consume exactly $4$ range checks. U32DIV performs two additional range checks for its remainder bound, as described below.

To perform these range checks, the prover puts the values into helper registers $h_0, ..., h_3$ and removes four unit-multiplicity RangeCheck messages from the typed LogUp relation described in the 16-bit range-check documentation. The fixed And8LookupAir table supplies the matching messages; there is no range-checker execution-trace component.

This operation is enforced via the following constraint. Note that since constraints cannot include divisions, the actual constraint which is enforced will be expressed equivalently with all denominators multiplied through, resulting in a constraint of degree 5.

$$b_{range}' = b_{range} - \frac{1}{R(h_0)} - \frac{1}{R(h_1)} - \frac{1}{R(h_2)} - \frac{1}{R(h_3)} \text{ | degree} = 5$$

Here $R$ is the challenge reduction for the typed RangeCheck message. The displayed equation is only the request side: And8LookupAir adds the matching table messages with their recorded multiplicities. It also omits the selector flag, which turns the request on only for the relevant operations.

Checking element validity

Another primitive which is required by most of the operations described below is checking whether four 16-bit values form a valid field element. Assume $t_0$, $t_1$, $t_2$, and $t_3$ are known to be 16-bit values, and we want to verify that $2^{48} \cdot t_3 + 2^{32} \cdot t_2 + 2^{16} \cdot t_1 + t_0$ is a valid field element.

For simplicity, let's denote:

$$v_{hi} = 2^{16} \cdot t_3 + t_2 v_{lo} = 2^{16} \cdot t_1 + t_0$$

We can then impose the following constraint to verify element validity:

$$\left(1 - m \cdot (2^{32} - 1 - v_{hi})\right) \cdot v_{lo} = 0 \text{ | degree} = 3$$

Where $m$ is a value set non-deterministically by the prover.

The above constraint should hold only if either of the following hold:

• $v_{lo} = 0$
• $v_{hi} \ne 2^{32} - 1$

To satisfy the latter equation, the prover needs to set $m = (2^{32} - 1 - v_{hi})^{-1}$, which is possible only when $v_{hi} \ne 2^{32} - 1$.

This constraint is sufficient because modulus $2^{64} - 2^{32} + 1$ in binary representation is 32 ones, followed by 31 zeros, followed by a single one:

$$1111111111111111111111111111111100000000000000000000000000000001$$

This implies that the largest possible 64-bit value encoding a valid field element would be 32 ones, followed by 32 zeros:

$$1111111111111111111111111111111100000000000000000000000000000000$$

Thus, for a 64-bit value to encode a valid field element, either the lower 32 bits must be all zeros, or the upper 32 bits must not be all ones (which is $2^{32} - 1$).

U32SPLIT

Assume $s_0$ is the element at the top of the stack. The U32SPLIT operation computes $(b,c) \leftarrow s_0$, where $b$ contains the lower 32 bits of $s_0$, and $c$ contains the upper 32 bits of $s_0$. The output stack is [b, c, ...] with $b$ (low limb) on top. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_0, ..., h_3$ to 16-bit limbs of $a$ with $h_0$ being the least significant limb. Thus, stack transition for this operation must satisfy the following constraints:

$$s_{0} = 2^{48} \cdot h_3 + 2^{32} \cdot h_2 + 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_{0}' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_{1}' = 2^{16} \cdot h_3 + h_2 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously. Also, we need to make sure that values in $h_0, ..., h_3$, when combined, form a valid field element, which we can do by putting a nondeterministic value $m$ into helper register $h_4$ and using the technique described here.

The effect of this operation on the rest of the stack is:

• Right shift starting from position $1$.

U32ASSERT2

Assume $s_0$ (top) and $s_1$ (next) are the elements at the top of the stack. The U32ASSERT2 verifies that both $s_0$ and $s_1$ are smaller than $2^{32}$. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_2$ and $h_3$ to low and high 16-bit limbs of $s_0$, and values in $h_0$ and $h_1$ to low and high 16-bit limbs of $s_1$. Thus, stack transition for this operation must satisfy the following constraints:

$$s_0' = 2^{16} \cdot h_3 + h_2 \text{ | degree} = 1$$ $$s_1' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously.

The effect of this operation on the rest of the stack is:

• No change starting from position $0$ - i.e., the state of the stack does not change.

U32ADD

Assume $s_0$ and $s_1$ are the values at the top of the stack which are known to be smaller than $2^{32}$. The U32ADD operation computes $(c,d) \leftarrow s_0 + s_1$, where $c$ contains the low 32-bits of the result, and $d$ is the carry bit. The output stack is [c, d, ...] with $c$ on top. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_0$, $h_1$, and $h_2$ to 16-bit limbs of $s_0 + s_1$ with $h_0$ being the least significant limb. Value in $h_3$ is set to $0$. Thus, stack transition for this operation must satisfy the following constraints:

$$s_0 + s_1 = 2^{32} \cdot h_2 + 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_0' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_1' = h_2 \text{ | degree} = 1$$ $$h_3 = 0 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously.

The effect of this operation on the rest of the stack is:

• No change starting from position $2$.

U32ADD3

Assume $s_0$, $s_1$, and $s_2$ are the values at the top of the stack which are known to be smaller than $2^{32}$. The U32ADD3 operation computes $(\mathsf{sum}, \mathsf{carry}) \leftarrow s_0 + s_1 + s_2$, where $\mathsf{sum}$ contains the low 32 bits of the result and $\mathsf{carry}$ contains the high 32 bits. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_0$, $h_1$, and $h_2$ to 16-bit limbs of $s_0 + s_1 + s_2$ with $h_0$ being the least significant limb. Value in $h_3$ is set to $0$. Thus, stack transition for this operation must satisfy the following constraints:

$$s_0 + s_1 + s_2 = 2^{32} \cdot h_2 + 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_0' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_1' = h_2 \text{ | degree} = 1$$ $$h_3 = 0 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously.

The effect of this operation on the rest of the stack is:

• Left shift starting from position $3$.

U32SUB

Assume $s_0$ and $s_1$ are the values at the top of the stack which are known to be smaller than $2^{32}$. The U32SUB operation computes $(\text{borrow}, \text{diff}) \leftarrow s_1 - s_0$, where diff contains the 32-bit result in two's complement, and borrow is the borrow bit. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_0$ and $h_1$ to the low and the high 16-bit limbs of $s_1 - s_0$ respectively. Values in $h_2$ and $h_3$ are set to $0$. Thus, stack transition for this operation must satisfy the following constraints:

$$s_1 = s_0 + s_1' - 2^{32} \cdot s_0' \text{ | degree} = 1$$ $$s_0'^2 - s_0' = 0 \text{ | degree} = 2$$ $$s_1' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously.

The effect of this operation on the rest of the stack is:

• No change starting from position $2$.

U32MUL

Assume $s_0$ and $s_1$ are the values at the top of the stack which are known to be smaller than $2^{32}$. The U32MUL operation computes $(c, d) \leftarrow s_0 \cdot s_1$, where $c$ and $d$ contain the low and the high 32-bits of the result respectively. The output stack is [c, d, ...] with $c$ on top. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_0, ..., h_3$ to 16-bit limbs of $s_0 \cdot s_1$ with $h_0$ being the least significant limb. Thus, stack transition for this operation must satisfy the following constraints:

$$s_0 \cdot s_1 = 2^{48} \cdot h_3 + 2^{32} \cdot h_2 + 2^{16} \cdot h_1 + h_0 \text{ | degree} = 2$$ $$s_0' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_1' = 2^{16} \cdot h_3 + h_2 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously. Also, we need to make sure that values in $h_0, ..., h_3$, when combined, form a valid field element, which we can do by putting a nondeterministic value $m$ into helper register $h_4$ and using the technique described here.

The effect of this operation on the rest of the stack is:

• No change starting from position $2$.

U32MADD

Assume $s_0$, $s_1$, and $s_2$ are the values at the top of the stack which are known to be smaller than $2^{32}$. The U32MADD operation computes $(\mathsf{lo}, \mathsf{hi}) \leftarrow s_0 \cdot s_1 + s_2$, where $\mathsf{lo}$ and $\mathsf{hi}$ contain the low and the high 32 bits of the result. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in $h_0, ..., h_3$ to 16-bit limbs of $s_0 \cdot s_1 + s_2$ with $h_0$ being the least significant limb. Thus, stack transition for this operation must satisfy the following constraints:

$$s_0 \cdot s_1 + s_2 = 2^{48} \cdot h_3 + 2^{32} \cdot h_2 + 2^{16} \cdot h_1 + h_0 \text{ | degree} = 2$$ $$s_0' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_1' = 2^{16} \cdot h_3 + h_2 \text{ | degree} = 1$$

In addition to the above constraints, we also need to verify that values in $h_0, ..., h_3$ are smaller than $2^{16}$, which we can do using 16-bit range checks as described previously. Also, we need to make sure that values in $h_0, ..., h_3$, when combined, form a valid field element, which we can do by putting a nondeterministic value $m$ into helper register $h_4$ and using the technique described here.

Note: that the above constraints guarantee the correctness of the operation iff $s_0 \cdot s_1 + s_2$ cannot overflow field modules (which is the case for the field with modulus $2^{64} - 2^{32} + 1$).

The effect of this operation on the rest of the stack is:

• Left shift starting from position $3$.

U32DIV

Assume the divisor $s_0$ is at the top of the stack and the dividend $s_1$ is below it, and both are smaller than $2^{32}$. The U32DIV operation computes $(r, q) \leftarrow s_1 / s_0$, where $r$ is the remainder and $q$ is the quotient.

To facilitate this operation, the prover sets values in $h_0$ and $h_1$ to the low and high 16-bit limbs of $q$, values in $h_2$ and $h_3$ to the low and high 16-bit limbs of $r$, and values in $h_4$ and $h_5$ to the low and high 16-bit limbs of $(s_0-r-1)$. Thus, the stack transition must satisfy the following constraints:

$$s_1 = s_0 \cdot s_1' + s_0' \text{ | degree} = 2$$ $$s_1' = 2^{16} \cdot h_1 + h_0 \text{ | degree} = 1$$ $$s_0' = 2^{16} \cdot h_3 + h_2 \text{ | degree} = 1$$ $$s_0 - s_0' - 1 = 2^{16} \cdot h_5 + h_4 \text{ | degree} = 1$$

All six helpers are range-checked to 16 bits. This directly bounds $q$ and $r$ to 32 bits, while the final constraint establishes $r < s_0$. The division identity therefore cannot wrap and determines the unique integer quotient and remainder.

The effect of this operation on the rest of the stack is:

• No change starting from position $2$.

U32AND

Assume $s_0$ and $s_1$ are the values at the top of the stack. The U32AND operation computes $c \leftarrow (s_0 \land s_1)$, where $c$ is the result of performing a bitwise AND on $s_0$ and $s_1$. The diagram below illustrates this graphically.

The operation removes one typed Bitwise message from the LogUp relation, with multiplicity $-1$:

$$[0,s_0,s_1,s'_0].$$

The leading $0$ selects AND. The bitwise chiplet adds the matching message with multiplicity $+1$.

Note: unlike for many other u32 operations, bitwise AND operation does not assume that the values at the top of the stack are smaller than $2^{32}$. This is because the lookup will fail for any inputs which are not 32-bit integers.

The effect of this operation on the rest of the stack is:

• Left shift starting from position $2$.

U32XOR

Assume $s_0$ and $s_1$ are the values at the top of the stack. The U32XOR operation computes $c \leftarrow (s_0 \oplus s_1)$, where $c$ is the result of performing a bitwise XOR on $s_0$ and $s_1$. The diagram below illustrates this graphically.

The operation removes one typed Bitwise message from the LogUp relation, with multiplicity $-1$:

$$[1,s_0,s_1,s'_0].$$

The leading $1$ selects XOR. The bitwise chiplet adds the matching message with multiplicity $+1$.

Note: unlike for many other u32 operations, bitwise XOR operation does not assume that the values at the top of the stack are smaller than $2^{32}$. This is because the lookup will fail for any inputs which are not 32-bit integers.

The effect of this operation on the rest of the stack is:

• Left shift starting from position $2$.