Multiset checks¶
A brief introduction to multiset checks can be found here. In Miden VM, multiset checks are used to implement virtual tables and efficient communication buses.
Running product columns¶
Although the multiset equality check can be thought of as comparing multiset equality between two vectors
- The running product column is initialized to a value
at the beginning of the trace. (We typically use .) - All values of
are multiplied into the running product column. - All values of
are divided out of the running product column. - If
and were multiset equal, then the running product column will equal at the end of the trace.
Running product columns are computed using a set of random values
Virtual tables¶
Virtual tables can be used to store intermediate data which is computed at one cycle and used at a different cycle. When the data is computed, the row is added to the table, and when it is used later, the row is deleted from the table. Thus, all that needs to be proved is the data consistency between the row that was added and the row that was deleted.
The consistency of a virtual table can be proved with a single trace column
The initial value of
Computing a virtual table’s trace column¶
To compute a product of rows, we’ll first need to reduce each row to a single value. This can be done as follows.
Let
The prover reduces row
Then, when row
Analogously, when row
Virtual tables in Miden VM¶
Miden VM makes use of 6 virtual tables across 4 components:
- Stack:
- Decoder:
- Chiplets:
- Chiplets virtual table, which combines the following two tables into one:
Communication buses via multiset checks¶
A bus
can be implemented as a single trace column
The values in this column contain a running product of the communication with the component as follows:
- Each request is “sent” by computing a lookup value from some information that’s specific to the specialized component, the operation inputs, and the operation outputs, and then dividing it out of the running product column
. - Each chiplet response is “sent” by computing the same lookup value from the component-specific information, inputs, and outputs, and then multiplying it into the running product column
.
Thus, if the requests and responses match, and the bus column
Note that the order of the requests and responses does not matter, as long as they are all included in
Communication bus constraints¶
These constraints can be expressed in a general way with the 2 following requirements:
- The lookup value must be computed using random values
, etc. that are provided by the verifier after the prover has committed to the main execution trace. - The lookup value must include all uniquely identifying information for the component/operation and its inputs and outputs.
Given an example operation
The constraint for sending this to the bus as a request would be:
The constraint for sending this to the bus as a response would be:
However, these constraints must be combined, since it’s possible that requests and responses both occur during the same cycle.
To combine them, let
The final constraint can be expressed as:
Communication buses in Miden VM¶
In Miden VM, the specialized components are implemented as dedicated segments of the execution trace, which include the 3 chiplets in the Chiplets module (the hash chiplet, bitwise chiplet, and memory chiplet).
Miden VM currently uses multiset checks to implement the chiplets bus