LogUp: multivariate lookups with logarithmic derivatives
The description of LogUp can be found here. In MidenVM, LogUp is used to implement efficient communication buses.
Using the LogUp construction instead of a simple multiset check with running products reduces the computational effort for the prover and the verifier. Given two columns and in the main trace where contains duplicates and does not (i.e. is part of the lookup table), LogUp allows us to compute two logarithmic derivatives and check their equality.
In the above:
- is the number of values in , which must be smaller than the size of the field. (The prime field used for Miden VM has modulus , so must be true.)
- is the number of values in , which must be smaller than the size of the field. (, for Miden VM)
- is the multiplicity of , which is expected to match the number of times the value is duplicated in column . It must be smaller than the size of the set of lookup values. ()
- is a random value that is sent to the prover by the verifier after the prover commits to the execution trace of the program.
Thus, instead of needing to compute running products, we are able to assert correct lookups by computing running sums.
Usage in Miden VM
The generalized trace columns and constraints for this construction are as follows, where component is some component in the trace and lookup table contains the values which need to be looked up from and how many times they are looked up (the multiplicity ).
Constraints
The diagrams above show running sum columns for computing the logarithmic derivatives for both and . As an optimization, we can combine these values into a single auxiliary column in the extension field that contains the running sum of values from both logarithmic derivatives. We'll refer to this column as a communication bus , since it communicates the lookup request from the component to the lookup table .
This can be expressed as follows:
Since constraints must be expressed without division, the actual constraint which is enforced will be the following:
In general, we will write constraints within these docs using the previous form, since it's clearer and more readable.
Additionally, boundary constraints must be enforced against to ensure that its initial and final values are . This will enforce that the logarithmic derivatives for and were equal.
Extending the construction to multiple components
The functionality of the bus can easily be extended to receive lookup requests from multiple components. For example, to additionally support requests from column , the bus constraint would be modified to the following:
Since the maximum constraint degree in Miden VM is 9, the lookup table could accommodate requests from at most 7 trace columns in the same trace row via this construction.
Extending the construction with flags
Boolean flags can also be used to determine when requests from various components are sent to the bus. For example, let be 1 when a request should be sent from and 0 otherwise, and let be similarly defined for column . We can use the following constraint to turn requests on or off:
If any of these flags have degree greater than 2 then this will increase the overall degree of the constraint and reduce the number of lookup requests that can be accommodated by the bus per row.