Usage
-Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.6 requires Rust version 1.67 or later.
+Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.7 requires Rust version 1.67 or later.
Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are:
- miden-processor, which can be used to execute Miden VM programs. diff --git a/print.html b/print.html index 045389d7ca..eb9d38fa28 100644 --- a/print.html +++ b/print.html @@ -174,7 +174,7 @@
- miden-processor, which can be used to execute Miden VM programs. @@ -1286,7 +1286,7 @@
- When stack depth is greater than :
-
@@ -3475,70 +3475,42 @@
- 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. -
- 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. -
- - 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. -
- 4 columns of the main trace: . +
- 3 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.
- 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. +
- 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.
- contains a binary value which differentiates between the 8-bit () and 16-bit () sections of the range checker's trace.
+
The range checker's execution trace looks as follows:
+
+
The columns have the following meanings:
-
-
- 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. +
- These values go from to . Values must either stay the same or increase by powers of 3 less than or equal to .
- 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.
@@ -3546,59 +3518,20 @@ - Value of in the first row is .
- Value of in the last row is .
- 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 value of in the first and last rows is . -
- The value of in the first and last rows is . @@ -4442,11 +4374,6 @@
A
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.
+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:
--
-
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:
--
-
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 .
+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. One way to do this could be to add bridge rows between two values to be range checked and add constraints to enforce the consistency of the gap between these bridge rows.
+If we allow gaps between two consecutive rows to only be 0 or powers of 2, we could enforce a constraint:
++
This constraint has a degree 9. This construction allows the minimum trace length to be 1024.
+We could go even further and allow the gaps between two consecutive rows to only be 0 or powers of 3. In this case we would enforce the constraint:
++
This allows us to reduce the minimum trace length to 64.
+To find out the number of bridge rows to be added in between two values to be range checked, we represent the gap between them as a linear combination of powers of 3, ie,
++
Then for each except the first, we add a bridge row at a gap of .
Miden approach
-This final optimized construction is implemented in Miden with the following requirements, capabilities, and constraints.
+This construction is implemented in Miden with the following requirements, capabilities and constraints.
Requirements
-
-
Capabilities
The construction gives us the following capabilities:
-
-
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:
--
-
Execution tra
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:
--
+-
Then, we need to constrain that the consecutive values in the range checker are either same or differ by powers of 3 less than or equal to .
-
+
In addition to the transition constraints described above, we also need to enforce the following boundary constraints:
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:
--
-
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:
--
-
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:
@@ -3609,12 +3542,11 @@Communica
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:
+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 .
+If is initialized to and the values sent to the bus by other VM components match those that are range-checked in the 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:
Op group table
Polygon Miden VM
Introduction
Miden VM is a zero-knowledge virtual machine written in Rust. For any program executed on Miden VM, a STARK-based proof of execution is automatically generated. This proof can then be used by anyone to verify that the program was executed correctly without the need for re-executing the program or even knowing the contents of the program.
Status and features
-Miden VM is currently on release v0.6. In this release, most of the core features of the VM have been stabilized, and most of the STARK proof generation has been implemented. While we expect to keep making changes to the VM internals, the external interfaces should remain relatively stable, and we will do our best to minimize the amount of breaking changes going forward.
+Miden VM is currently on release v0.7. In this release, most of the core features of the VM have been stabilized, and most of the STARK proof generation has been implemented. While we expect to keep making changes to the VM internals, the external interfaces should remain relatively stable, and we will do our best to minimize the amount of breaking changes going forward.
At this point, Miden VM is good enough for experimentation, and even for real-world applications, but it is not yet ready for production use. The codebase has not been audited and contains known and unknown bugs and security flaws.
Feature highlights
Miden VM is a fully-featured virtual machine. Despite being optimized for zero-knowledge proof generation, it provides all the features one would expect from a regular VM. To highlight a few:
@@ -248,7 +248,7 @@
Usage
-Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.6 requires Rust version 1.67 or later.
+Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.7 requires Rust version 1.67 or later.
Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are:
VM components
The above components are connected via buses, which are implemented using multiset checks. We also use multiset checks internally within components to describe virtual tables.
VM execution trace
-The execution trace of Miden VM consists of main trace columns, buses, and virtual tables, as shown in the diagram below.
+The execution trace of Miden VM consists of main trace columns, buses, and virtual tables, as shown in the diagram below.
As can be seen from the above, the system, decoder, stack, and range checker components use dedicated sets of columns, while all chiplets share the same columns. To differentiate between chiplets, we use a set of binary selector columns, a combination of which uniquely identifies each chiplet.
The system component does not yet have a dedicated documentation section, since the design is likely to change. However, the following two columns are not expected to change:
@@ -2252,7 +2252,7 @@ Right shift
Left shift
If an operation removes an item from the stack, we say that the operation caused a left shift. For example, a DROP operation causes a left shift. Assuming the stack is in the state we left it at the end of the previous section, graphically, this looks like so:
-Overall, the during the left shift we do the following:
+Overall, during the left shift we do the following:
VM components
DROP operation causes a left shift. Assuming the stack is in the state we left it at the end of the previous section, graphically, this looks like so: