# 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.

### 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 ). The number of required range checks varies between and , depending on the operation. However, to simplify the constraint system, we force each relevant operation to consume exactly range checks.

To perform these range checks, the prover puts the values to be range-checked into helper registers , and then updates the range checker bus column according to the LogUp construction described in the range checker documentation, using multiplicity for each value.

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.

The above is just a partial constraint as it does not show the range checker's part of the constraint, which adds the required values into the bus column. It also omits the selector flag which is used to turn this constraint on only when executing 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 , , , and are known to be 16-bit values, and we want to verify that is a valid field element.

For simplicity, let's denote:

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

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

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

To satisfy the latter equation, the prover needs to set , which is possible only when .

This constraint is sufficient because modulus in binary representation is 32 ones, followed by 31 zeros, followed by a single one:

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

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 ).

## U32SPLIT

Assume is the element at the top of the stack. The U32SPLIT operation computes , where contains the lower 32 bits of , and contains the upper 32 bits of . The diagram below illustrates this graphically.

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

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

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

• Right shift starting from position .

## U32ASSERT2

Assume and are the elements at the top of the stack. The U32ASSERT2 verifies that both and are smaller than . The diagram below illustrates this graphically.

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

In addition to the above constraints, we also need to verify that values in are smaller than , 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 - i.e., the state of the stack does not change.

Assume and are the values at the top of the stack which are known to be smaller than . The U32ADD operation computes , where contains the low 32-bits of the result, and is the carry bit. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in , , and to 16-bit limbs of with being the least significant limb. Value in is set to . Thus, stack transition for this operation must satisfy the following constraints:

In addition to the above constraints, we also need to verify that values in are smaller than , 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 .

Assume , , are the values at the top of the stack which are known to be smaller than . The U32ADD3 operation computes , where and contains the low and the high 32-bits of the result respectively. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in , , and to 16-bit limbs of with being the least significant limb. Value in is set to . Thus, stack transition for this operation must satisfy the following constraints:

In addition to the above constraints, we also need to verify that values in are smaller than , 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 .

## U32SUB

Assume and are the values at the top of the stack which are known to be smaller than . The U32SUB operation computes , where contains the 32-bit result in two's complement, and is the borrow bit. The diagram below illustrates this graphically.

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

In addition to the above constraints, we also need to verify that values in are smaller than , 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 .

## U32MUL

Assume and are the values at the top of the stack which are known to be smaller than . The U32MUL operation computes , where and contain the low and the high 32-bits of the result respectively. The diagram below illustrates this graphically.

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

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

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

• No change starting from position .

Assume , , are the values at the top of the stack which are known to be smaller than . The U32MADD operation computes , where and contains the low and the high 32-bits of . The diagram below illustrates this graphically.

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

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

Note: that the above constraints guarantee the correctness of the operation iff cannot overflow field modules (which is the case for the field with modulus ).

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

• Left shift starting from position .

## U32DIV

Assume and are the values at the top of the stack which are known to be smaller than . The U32DIV operation computes , where contains the quotient and contains the remainder. The diagram below illustrates this graphically.

To facilitate this operation, the prover sets values in and to 16-bit limbs of , and values in and to 16-bit limbs of . Thus, stack transition for this operation must satisfy the following constraints:

The second constraint enforces that , while the third constraint enforces that .

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

• No change starting from position .

## U32AND

Assume and are the values at the top of the stack. The U32AND operation computes , where is the result of performing a bitwise AND on and . The diagram below illustrates this graphically.

To facilitate this operation, we will need to make a request to the chiplet bus by dividing its current value by the value representing bitwise operation request. This can be enforced with the following constraint:

In the above, is the unique operation label of the bitwise AND operation.

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 . 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 .

## U32XOR

Assume and are the values at the top of the stack. The U32XOR operation computes , where is the result of performing a bitwise XOR on and . The diagram below illustrates this graphically.

To facilitate this operation, we will need to make a request to the chiplet bus by dividing its current value by the value representing bitwise operation request. This can be enforced with the following constraint:

In the above, is the unique operation label of the bitwise XOR operation.

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 . 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 .