Range Checker
Miden VM relies very heavily on 16-bit range-checks (checking if a value of a field element is between and ). For example, most of the u32 operations, need to perform between two and four 16-bit range-checks per operation. Similarly, operations involving memory (e.g. load and store) require two 16-bit range-check per operation.
Thus, it is very important for the VM to be able to perform a large number 16-bit range checks very efficiently. In this note we describe how this can be achieved using permutation checks.
8-bit range checks
First, let's define a construction for the simplest possible 8-bit range-check. This can be done with a single column as illustrated below.
For this to work as a range-check we need to enforce a few constraints on this column:
- Value in the first row must be .
- Value in the last row must be .
- As we move from one row to the next, we can either keep the value the same, or increment it by .
Denoting as the value of column in the current row, and as the value of column in the next row, we can enforce the last condition as follows:
Together, these constraints guarantee that all values in column are between and (inclusive).
We can then add another column , which will keep a running product of values in offset by random value (provided by the verifier). Transition constraints for column would look like so:
Using these two columns we can check if some other column in the execution trace is a permutation of values in . Let's call this other column . We can compute the running product of in the same way as we compute the running product for . Then, we can check that the last value in is the same as the final value for the running product of (this is the permutation check).
While this approach works, it has a couple of limitations:
- First, column must contain all values between and . Thus, if column does not contain one of these values, we need to artificially add this value to somehow (i.e., we need to pad with extra values).
- Second, assuming is the length of execution trace, we can range-check at most values. Thus, if we wanted to range-check more than values, we'd need to introduce another column similar to .
To get rid of the padding requirement, we can add a selector column, which would contain for values we want to include in the running product, and for the ones we don't. But we can address both issues with a single solution.
A better construction
Let's add two selector column to our table and as illustrated below.
The purpose of these columns is as follows:
- When and , we won't include the value into the running product.
- When and , we will include the value into the running product.
- When and , we will include two copies of the value into the running product.
- When and , we will include four copies of the value into the running product.
Thus, for the table pictured below, the running product will include: a single , a single , no 's, and five 's etc.
To keep the description of constraints simple, we'll first define the four flag values as follows:
Thus, for example, when and , and .
Then, we'll update transition constraints for like so:
The above ensures that when , remains the same, when , is multiplied by , when , is multiplied by , and when , is multiplied by .
We also need to ensure that values in columns and are binary (either or ). This can be done with the following constraints:
And lastly, for completeness, we still need to impose a transition constraint that we had in the naive approach:
This 3-column table addresses the limitations we had as follows:
- We no longer need to pad the column we want to range-check with extra values because we can skip the values we don't care about.
- We can support almost range checks (when is relatively large). Though, for short traces (when ), we can range-check at most unique values.
The one downside of this approach is that the degree of our constraints is now (vs. in the naive approach). But in the context of Miden VM this doesn't matter as maximum constraint degree for the VM is anyway.
16-bit range checks
To support 16-bit range checks, let's try to extend the idea of the 8-bit table. Our 16-bit table would look like so (the only difference is that column now has to end with value ):
While this works, it is rather wasteful. In the worst case, we'd need to enumerate over 65K values, most of which we may not actually need. It would be nice if we could "skip over" the values that we don't want. We can do this by relying on 8-bit range checks. Specifically, instead of enforcing constraint:
We would enforce:
Where is another running product column. At the end of the execution trace, we would check that . This would ensure that as we move from one row to another, values in column increase by at most (we are basically performing an 8-bit range check on increments of column ). Now, our table can look like this:
We still may need to include some unneeded rows because we can not "jump" by more than values, but at least we are guaranteed that the number of such unneeded rows will never be greater than .
We also need to add another running product column to support permutation checks against column . The constraint that we'll need to impose against this column is identical to the constraint we imposed against column and will look like so:
Overall, with this construction we have the following:
- We need two table of three columns each ( columns total), and we need running product columns.
- This gives us the ability to do the following:
- For long traces (when ) we can support almost arbitrary 16-bit range-checks.
- For short traces, we can range-check at most unique values, but if there are duplicates, we can support up to total range-checks.
But we can do better.
Optimizations
First, we can just stack the tables on top of each other. We'll need to add a column to partition the table between the sections used for 8-bit range checks and sections used for 16-bit range checks. Let's call this column . When , we'll apply constraints for the 8-bit table, and when , we'll apply constraints for the 16-bit table.
Second, we can merge running product columns and into a single column. We'll do it like so:
- When , we'll multiply the current value of the column by the 8-bit value (offset by random ) that we want to add into the running product.
- When , we'll divide the current value of the column by the 8-bit value (offset by random ) which we'd like to remove from the running product.
In the end, if we added and then removed all the same values, the value in this column (let's call it ) should equal to , and we can check this condition via a boundary constraint.
The only downside of this construction is again higher constraint degree. Specifically, some of the transition constraints described above have degree . However, this doesn't matter in the context of Miden VM, since the max constraint degree of the VM is .
Miden approach
This final optimized construction is implemented in Miden with the following requirements, capabilities, and constraints.
Requirements
- 4 columns of the main trace: .
- 1 bus to ensure that the range checks performed in the range checker match those requested by other VM components (the stack and the memory chiplet).
- 1 virtual table, tracked in running product column , which enables skipping values by up to in the 16-bit section of the trace and enforces consistency between the range checks in the 8-bit section of the trace and the value increments in the 16-bit section of the trace.
Capabilities
The construction gives us the following capabilities:
- For long traces (when ), we can do over arbitrary 16-bit range-checks.
- For short traces (), we can range-check at slightly fewer than unique values, but if there are duplicates, we may be able to range-check up to total values.
Execution trace
The range checker's execution trace looks like the table described in the optimizations section above.
As previously described, the columns have the following meanings:
- contains a binary value which differentiates between the 8-bit () and 16-bit () sections of the range checker's trace.
- The 8-bit section of the trace contains the range checks required to ensure internal consistency of the Range Checker.
- The 16-bit section of the trace contains the range checks required by other components (e.g. the stack and the memory chiplet).
- and are selector columns that are combined into flags to indicate the number of times the value in that row should be range checked (included into the running product). With these flags, values can be included 0, 1, 2, or 4 times per row in the execution trace. (Values can be included more times by having multiple trace rows with the same value).
- contains the values to be range checked.
- During the 8-bit section of the trace (when ), these values go from to and must either stay the same or increase by one at each step.
- During the 16-bit section of the trace (when ), these values go from to . Values must either stay the same or increase by less than at each step.
- The final 2 rows of the 16-bit section of the trace must both equal . The extra value of is required in order to pad the trace so the running product bus column can be computed correctly.
Execution trace constraints
First, we'll need to make sure that all selector flags are binary. This can be done with the following constraints:
Next, we need to constrain the row transitions in the 8-bit section of the table so that as we move from one row to the next the value either stays the same or increases by 1.
Next, we need to make sure that values in column can "flip" from to only once. The following constraint enforces this:
Finally, we need to make sure that when column "flips" from to (we are moving from the 8-bit section of the table to the 16-bit section), the current value in column is equal to , and the next value is reset to . This can be done with the following constraints:
In addition to the transition constraints described above, we also need to enforce the following boundary constraints:
- Value of in the first row is .
- Value of in the last row is .
8-bit range checks table
The 8-bit range checks virtual table is used to enforce the internal correctness of the 16-bit section of the Range Checker (where range checks for user operations and other components are executed).
This table can be thought of as a virtual table that contains all 8-bit range checks required to ensure correctness of the 16-bit section:
- When a value is range-checked in the 8-bit section of the trace (i.e., the flag indicates that it should be included 1, 2, or 4 times), it is added to the virtual table. The value must be added to the virtual table as many times as that row's flag indicates it should be range-checked.
- In the 16-bit section of the trace, a single 8-bit range check on is required at each step. Therefore, a single 8-bit range check of is removed from the virtual table at each step.
The running product column is used to keep track of the state of the table.
To simplify the notation, we'll first define variable , which represents how a row in the execution trace is reduced to a single value.
In the 8-bit section (), one, two, or four 8-bit range checks are added to the virtual table at each step and is updated as follows:
Note that if is true then the value of does not change, so no 8-bit range checks are added to the virtual table.
In the 16-bit section (), one 8-bit range check is removed from the virtual table at each step and is updated as follows:
The above actually enforces that .
These two updates, which first build up the product and then reduce it, can be combined into a single constraint:
Thus, if the prover arranged the 8-bit and the 16-bit sections of the table correctly and was initialized to , we should end up with at the end of the trace.
In addition to the transition constraints described above, we also need to enforce the following boundary constraint:
- The value of in the first and last rows is .
Communication bus
is the bus that connects components which require 16-bit range checks to the range-checked values in the 16-bit section of the range checker. The bus constraints are defined by the components that use it to communicate.
Requests are sent to the range checker bus by the following components:
- The Stack sends requests for 16-bit range checks during some
u32
operations. - The Memory chiplet sends requests for 16-bit range checks against the values in the and trace columns to enforce internal consistency.
Responses are provided by the range checker as follows.
Once again, we'll make use of variable , which represents how a row in the execution trace is reduced to a single value.
Only the 16-bit section of the trace should be included in the bus column. Transition constraints for this are fairly straightforward:
Thus, when , the value in does not change, but when , the next value in is computed by multiplying the current value by .
If is initialized to and the values sent to the bus by other VM components match those that are range-checked in the 16-bit section of the trace, then at the end of the trace we should end up with .
In addition to the transition constraint described above, we also need to enforce the following boundary constraint:
- The value of in the first and last rows is .