# Memory Models & Lookup Arguments in leanVM

## Memory in the leanVM

The primary goal of the leanVM is to prove the aggregation and merging of many hash-based signatures (XMSS). This requires a VM that can execute logic involving loops, function calls, and data access.

The leanVM design opts for a **Read-Only Memory** model.
* **Advantage**: It's simpler and cheaper to prove. The Prover can't overwrite memory, which simplifies the constraints.
* **Challenge**: How do we efficiently prove that the Prover's memory operations are valid?

A memory trace is considered valid if it satisfies two core properties:
1. **Read-Only Property**: The same memory address must always return the same value. An access $(a, v)$ is inconsistent if another access $(a, v')$ exists where $v \neq v'$.
2. **Continuity Property** (for some use cases): The set of all accessed memory addresses forms a complete, contiguous range.

Enforcing these properties directly on a raw, unsorted memory trace is difficult. The key insight is to prove that the memory trace is a **permutation** of a sorted, valid memory layout. This transforms the problem of verifying memory consistency into a **multiset check**.

## Technique 1: The Permutation Check (Grand Product Argument)

A multiset check verifies that two multisets (sets that allow repeated elements) are equal. In our context, we want to prove:
> *The multiset of address-value pairs $(a, v)$ used in the execution is a permutation of a sorted and valid set of pairs $(a', v')$.*

### The Core Idea: Polynomial Equivalence
We can represent each multiset as a polynomial whose roots are the elements of the multiset. If the two multisets are equal, their corresponding polynomials will be identical.

Given two multisets $\{x_i\}$ and $\{y_i\}$, we check the following polynomial identity by evaluating it at a random challenge $\alpha$:
$$\prod_{i} (\alpha - x_i) \stackrel{?}{=} \prod_{i} (\alpha - y_i)$$
This check is made practical in a STARK using a **running product column**. We introduce an auxiliary column `p` in our AIR table that enforces this check across all rows.

* **Initialization (Boundary Constraint)**: `p[0] = 1`.
* **Update Rule (Transition Constraint)**:
$$
p[i+1] = p[i] \cdot \frac{\alpha - x_i}{\alpha - y_i}
$$
* **Final Check (Boundary Constraint)**: `p[last] = 1`.

If the final value of the running product is 1, it means all terms in the numerator have been canceled out by terms in the denominator, proving the two multisets are identical. This powerful technique is often called a **Grand Product Argument**.

### Open Questions for Discussion
* The Grand Product argument works well but can be rigid. What are its main limitations, especially when dealing with repeated operations or values with varying frequencies?
* How does the degree of the transition constraint impact prover performance, and what happens to it here?

## Technique 2: LogUp - Handling Multiplicities

The Grand Product argument breaks down when we need to handle **multiplicities** efficiently. For example, a range check table might contain the value `5` only once, but the execution trace might use it 100 times. We need a way to check that `5` appears in the table while accounting for its 100 uses.

The multiset check with multiplicities is:
$$\prod_{i} (\alpha - x_i) = \prod_{j} (\alpha - t_j)^{m_j}$$
where $m_j$ is the number of times table element $t_j$ is used. This is not a polynomial equation because the multiplicity $m_j$ is in the exponent.

### The LogUp: Products to Sums
**LogUp** elegantly solves this by applying a formal logarithmic derivative, which transforms products into sums:
$$\frac{d}{d\alpha} \log \left( \prod (\alpha - x_i) \right) = \sum \frac{1}{\alpha - x_i}$$
The multiset check with multiplicities becomes a polynomial-friendly equation:
$$\sum_{i} \frac{1}{\alpha - x_i} \stackrel{?}{=} \sum_{j} \frac{m_j}{\alpha - t_j}$$
This is implemented with a **running sum** column `s` instead of a running product column.

* **Initialization**: `s[0] = 0`.
* **Update Rule**: $s[i+1] = s[i] + \frac{m_{i+1}}{\alpha - t_{i+1}} - \frac{1}{\alpha - x_{i+1}}$.
* **Final Check**: `s[last] = 0`.

### The Trade-off
While super nice, LogUp has a significant drawback: **higher-degree constraints**. To eliminate the fractions in the transition constraint, we multiply by all denominators, causing the degrees of the polynomials involved to add up. This increases prover complexity and can impact performance.

### Open Questions for Discussion
* When is the complexity of LogUp justified over a simpler Grand Product? What are the key design trade-offs?
* Are there techniques to mitigate the degree explosion in LogUp constraints?
* Is there any benefit to add LogUp+GKR? It seems Starkware and Miden folks abandoned this idea after testing it.

## Technique 3: LogUp* - Optimizing Indexed Lookups

The leanVM, like many modern zk-VMs, needs to perform indexed lookups. For example, to decode an instruction, it looks up flags and offsets from a small, fixed bytecode table.

* **The Table $T$**: A small table of size $m$ (e.g., the VM's instruction set).
* **The Index Column $I$**: A large column of size $n$ in the execution trace, specifying which instruction is executed at each cycle.
* **The Looked-Up Values $I*T$**: The resulting values, where $(I*T)[i] = T[I[i]]$.

The challenge is that $I*T$ is a large vector ($n$ elements) of potentially large field elements. Committing to $I*T$ directly is very expensive for the Prover.

### Pushforward/Pullback
**LogUp*** avoids committing to $I*T$ entirely by using pushforward/pullback.

* **Pullback $I*T$**: "Pulls" values *from* the table $T$ according to indices in $I$. This creates the large vector we want to avoid.
* **Pushforward $I_*A$**: "Pushes" and aggregates values *from* a vector $A$ *to* the table $T$'s structure. This creates a small vector of size $m$.
$$
(I_*A)[j] = \sum_{i \text{ s.t. } I[i]=j} A[i]
$$

The core duality lemma states: $\langle I_* A, B \rangle = \langle A, I^* B \rangle$.

### The LogUp* Protocol
To prove a claim about an evaluation of $I*T$ at a random point $r$, e.g., $(I*T)(r) = e$, the protocol is:

1. **Commit**: The Prover commits to the small vectors $I$ and $T$, and the small pushforward vector $I_*eq_r$, where $eq_r$ is a special evaluation polynomial (the Lagrange kernel). Importantly, the Prover never commits to the large $I*T$ vector.
2. **Prove**: The Prover uses the duality lemma to transform the claim:
$$
e = (I^*T)(r) = \langle I^*T, eq_r \rangle = \langle T, I_*eq_r \rangle
$$
This final claim, $\langle T, I_*eq_r \rangle = e$, is an inner product between two small, committed vectors. It can be verified efficiently with a sumcheck protocol.
3. **Validate**: The Prover must also prove that the $I_*eq_r$ vector was computed correctly. This is done with a specialized LogUp-style check on the pushforward.

This trades one large commitment for one small commitment and a sumcheck, resulting in a massive performance gain for the Prover. The leanVM uses logup* to handle instruction decoding by looking up flags and offsets from its bytecode, significantly reducing commitment costs.

### Open Questions for Discussion
* LogUp* seems ideal for small tables. What defines "small"? What is the break-even point where this technique becomes more efficient than others?
* The protocol involves a sumcheck. How does the cost of this sumcheck compare to the savings from avoiding the commitment to $I*T$?
* A classical LogUp is much more simple, is LogUp* worth it in practice (we should have feedback on this since we already have benchmarks with LogUp* but not sure we tested the simplest LogUp solution for now)?

## Broader Implementation Questions

Let's zoom out and consider the bigger picture.

* **Packing Polynomials**: The leanVM design mentions "Jagged PCS" and "Simple Packing" to avoid committing to many separate AIR columns. How do these techniques relate to lookups? Are they complementary or competing?
* **Unified Primitives**: Can we design a single, generic lookup/multiset check primitive that can be configured for Grand Product, LogUp, or LogUp* based on the use case? What would the API for such a primitive look like?
* How can we best integrate these advanced lookup arguments into a modular proof system like Plonky3, ensuring both performance and developer-friendliness?