Skip to main content
Version: 0.12 (unstable)

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 aa and bb in the main trace where aa contains duplicates and bb does not (i.e. bb is part of the lookup table), LogUp allows us to compute two logarithmic derivatives and check their equality.

i=0l1(αai)=i=0nmi(αbi)\sum_{i=0}^{l} \frac{1}{(\alpha - a_i)} = \sum_{i=0}^{n} \frac{m_i}{(\alpha - b_i)}

In the above:

  • ll is the number of values in aa, which must be smaller than the size of the field. (The prime field used for Miden VM has modulus p=264232+1p = 2^{64} - 2^{32} + 1, so l<pl < p must be true.)
  • nn is the number of values in bb, which must be smaller than the size of the field. (n<pn < p, for Miden VM)
  • mim_i is the multiplicity of bib_i, which is expected to match the number of times the value bib_i is duplicated in column aa. It must be smaller than the size of the set of lookup values. (mi<nm_i < n)
  • α\alpha 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 XX is some component in the trace and lookup table TT contains the values vv which need to be looked up from XX and how many times they are looked up (the multiplicity mm).

logup_component_x

logup_table_t

Constraints

The diagrams above show running sum columns for computing the logarithmic derivatives for both XX and TT. 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 bb, since it communicates the lookup request from the component XX to the lookup table TT.

This can be expressed as follows:

b=b+m(αv)1(αx)b' = b + \frac{m}{(\alpha - v)} - \frac{1}{(\alpha - x)}

Since constraints must be expressed without division, the actual constraint which is enforced will be the following:

b(αv)(αx)=b(αx)(αv)+m(αx)(αv) | degree=3b' \cdot (\alpha - v) \cdot (\alpha - x) = b \cdot (\alpha - x) \cdot (\alpha - v) + m \cdot (\alpha - x) - (\alpha - v) \text{ | degree} = 3

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 bb to ensure that its initial and final values are 11. This will enforce that the logarithmic derivatives for XX and TT 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 yy, the bus constraint would be modified to the following:

b=b+m(αv)1(αx)1(αy) | degree=4b' = b + \frac{m}{(\alpha - v)} - \frac{1}{(\alpha - x)} - \frac{1}{(\alpha - y)} \text{ | degree} = 4

Since the maximum constraint degree in Miden VM is 9, the lookup table TT 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 fxf_x be 1 when a request should be sent from xx and 0 otherwise, and let fyf_y be similarly defined for column yy. We can use the following constraint to turn requests on or off:

b=b+m(αv)fx(αx)fy(αy) | degree=4b' = b + \frac{m}{(\alpha - v)} - \frac{f_x}{(\alpha - x)} - \frac{f_y}{(\alpha - y)} \text{ | degree} = 4

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.